pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Change ProofByReflection to work in Coq 8.6.1

Browse source
This commit is contained in:
Adam Chlipala 2017-11-18 10:43:08 -05:00
parent 19e9e84953
commit 1ee699431c
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -10,6 +10,7 @@
*.ilg *.ilg
*.ind *.ind
Makefile.coq Makefile.coq
Makefile.coq.conf
*.glob *.glob
*.v.d *.v.d
*.vo *.vo

4
ProofByReflection.v
View file

@ -497,7 +497,9 @@ Ltac simplify_set :=
match goal with match goal with
| [ |- context[?X \cup ?Y] ] => | [ |- context[?X \cup ?Y] ] =>
let e := reify_set (X \cup Y) in let e := reify_set (X \cup Y) in
change (X \cup Y) with (setexprDenote e); let Heq := fresh in
assert (Heq : X \cup Y = setexprDenote e) by reflexivity;
rewrite Heq; clear Heq;
rewrite normalize_ok; simpl rewrite normalize_ok; simpl
end. end.