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

SepCancel: adapt for Coq versions

Browse source
This commit is contained in:
Adam Chlipala 2016-04-20 08:36:48 -04:00
parent 2dc04da2b9
commit 47fd9a8abf
1 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
SepCancel.v
View file

@ -308,8 +308,24 @@ Module Make(Import S : SEP).
reflexivity. reflexivity.
Qed. Qed.
Module Type TRY_ME_FIRST.
Parameter try_me_first : hprop -> Prop.
Axiom try_me_first_easy : forall p, try_me_first p.
End TRY_ME_FIRST.
Module TMF : TRY_ME_FIRST.
Definition try_me_first (_ : hprop) := True. Definition try_me_first (_ : hprop) := True.
Theorem try_me_first_easy : forall p, try_me_first p.
Proof.
constructor.
Qed.
End TMF.
Import TMF.
Export TMF.
Ltac cancel1 := Ltac cancel1 :=
match goal with match goal with
| [ |- ?p ===> ?q ] => | [ |- ?p ===> ?q ] =>