Skip to content

Commit

Permalink
Merge pull request #131 from JasonGross/patch-1
Browse files Browse the repository at this point in the history 
GhostSimulations:Be more robust to generated names
  • Loading branch information
@palmskog
palmskog authored Oct 26, 2021
2 parents c808a15 + dfd9958 commit 064cc4f
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions core/GhostSimulations.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ Definition deghost (net : @network _ refined_multi_params) : (@network _ multi_p
_
).
intros.
destruct net.
destruct net as [? nwState].
concludes.
destruct nwState. auto.
Defined.
Expand Down Expand Up @@ -249,7 +249,7 @@ Definition reghost (net : @network _ multi_params) : @network _ refined_multi_pa
_
).
intros.
destruct net.
destruct net as [? nwState].
concludes.
exact (ghost_init, nwState).
Defined.
Expand Down

2 comments on commit 064cc4f

@brando90
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for which coq version does this work?

@hackedy
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for which coq version does this work?

The supported Coq versions are specified in the OPAM file.

verdi/coq-verdi.opam

Line 25 in 064cc4f

"coq" {(>= "8.7" & < "8.12~") | (= "dev")}

If you look at the commits in the output of of git log ./coq-verdi.opam you'll see that the supported Coq versions went straight from 8.11 to 8.14+, skipping 8.12 and 8.13.

Please sign in to comment.