From 47fd9a8abf3f398277ae5b1730125376230393c3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 20 Apr 2016 08:36:48 -0400 Subject: [PATCH] SepCancel: adapt for Coq versions --- SepCancel.v | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/SepCancel.v b/SepCancel.v index 3f9194a..e194307 100644 --- a/SepCancel.v +++ b/SepCancel.v @@ -308,7 +308,23 @@ Module Make(Import S : SEP). reflexivity. Qed. - Definition try_me_first (_ : hprop) := True. + 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. + + Theorem try_me_first_easy : forall p, try_me_first p. + Proof. + constructor. + Qed. + End TMF. + + Import TMF. + Export TMF. Ltac cancel1 := match goal with