From bd306f5b046565c9f1bbb1bb6b6b9343beede52c Mon Sep 17 00:00:00 2001 From: minki Date: Sun, 3 Feb 2019 03:00:28 +0900 Subject: [PATCH] hotfix for coq 8.6 --- metasrc/pacon.v | 6 +++--- src/pacon.v | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/metasrc/pacon.v b/metasrc/pacon.v index a9e0327..0e724c2 100644 --- 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 index a9e0327..0e724c2 100644 --- 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 ]. -