hotfix for coq 8.6

snu-sf · Feb 2, 2019 · bd306f5 · bd306f5
1 parent 0bb3ee0
commit bd306f5
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/metasrc/pacon.v b/metasrc/pacon.v
@@ -36,7 +36,7 @@ Notation "p <_paco_1= q" :=
 (* coinduction automation - internal use only *)
 Ltac paco_cofix_auto :=
   let CIH := fresh "CIH" in cofix CIH; repeat intro;
-  match goal with [H: _ |- _] => destruct H as [[]] end; do 2 econstructor;
+  match goal with [H: _ |- _] => apply paco_observe in H; destruct H as [] end; do 2 econstructor;
   try (match goal with [H: _|-_] => apply H end); intros;
   lazymatch goal with [PR: _ |- _] => match goal with [H: _ |- _] => apply H in PR end end;
   repeat match goal with [ H : _ \/ _ |- _] => destruct H end; first [eauto; fail|eauto 10].
@@ -65,6 +65,7 @@ Proof.
   clear PR; repeat (try left; do 2 paco_revert; paco_cofix_auto).
 Qed.
 
+
 Theorem paco_mon: monotone (paco gf).
 Proof. paco_cofix_auto; repeat (left; do 2 paco_revert; paco_cofix_auto). Qed.
 
@@ -82,7 +83,7 @@ Proof. intros; do 2 econstructor; [ |eauto]; eauto. Qed.
 
 Theorem paco_unfold: forall (MON: monotone gf) r,
   paco gf r <1= gf (upaco gf r).
-Proof. unfold monotone; intros; destruct PR as [[]]; eauto. Qed.
+Proof. unfold monotone; intros; apply paco_observe in PR; destruct PR as []; eauto. Qed.
 
 Theorem _paco_acc: forall
   l r (OBG: forall rr (INC: r <1== rr) (CIH: l <1== rr), l <1== paco gf rr),
@@ -118,4 +119,3 @@ Arguments paco_mult_strong    [ T0 ].
 Arguments paco_mult           [ T0 ].
 Arguments paco_fold           [ T0 ].
 Arguments paco_unfold         [ T0 ].
-
diff --git a/src/pacon.v b/src/pacon.v
@@ -36,7 +36,7 @@ Notation "p <_paco_1= q" :=
 (* coinduction automation - internal use only *)
 Ltac paco_cofix_auto :=
   let CIH := fresh "CIH" in cofix CIH; repeat intro;
-  match goal with [H: _ |- _] => destruct H as [[]] end; do 2 econstructor;
+  match goal with [H: _ |- _] => apply paco_observe in H; destruct H as [] end; do 2 econstructor;
   try (match goal with [H: _|-_] => apply H end); intros;
   lazymatch goal with [PR: _ |- _] => match goal with [H: _ |- _] => apply H in PR end end;
   repeat match goal with [ H : _ \/ _ |- _] => destruct H end; first [eauto; fail|eauto 10].
@@ -65,6 +65,7 @@ Proof.
   clear PR; repeat (try left; do 2 paco_revert; paco_cofix_auto).
 Qed.
 
+
 Theorem paco_mon: monotone (paco gf).
 Proof. paco_cofix_auto; repeat (left; do 2 paco_revert; paco_cofix_auto). Qed.
 
@@ -82,7 +83,7 @@ Proof. intros; do 2 econstructor; [ |eauto]; eauto. Qed.
 
 Theorem paco_unfold: forall (MON: monotone gf) r,
   paco gf r <1= gf (upaco gf r).
-Proof. unfold monotone; intros; destruct PR as [[]]; eauto. Qed.
+Proof. unfold monotone; intros; apply paco_observe in PR; destruct PR as []; eauto. Qed.
 
 Theorem _paco_acc: forall
   l r (OBG: forall rr (INC: r <1== rr) (CIH: l <1== rr), l <1== paco gf rr),
@@ -118,4 +119,3 @@ Arguments paco_mult_strong    [ T0 ].
 Arguments paco_mult           [ T0 ].
 Arguments paco_fold           [ T0 ].
 Arguments paco_unfold         [ T0 ].
-