diff options
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1416.v | 27 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1501.v | 12 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1596.v | 16 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1671.v | 2 |
4 files changed, 15 insertions, 42 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v deleted file mode 100644 index c6f4302d..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1416.v +++ /dev/null @@ -1,27 +0,0 @@ -Set Implicit Arguments. - -Record Place (Env A: Type) : Type := { - read: Env -> A ; - write: Env -> A -> Env ; - write_read: forall (e:Env), (write e (read e))=e -}. - -Hint Rewrite -> write_read: placeeq. - -Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type := - { - mkEnv: A -> B -> Env ; - mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x) - }. - -(* when the following line is commented, the bug does not appear *) -Hint Rewrite -> mkEnv2writeL: placeeq. - -Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A), - (exists e1:Env, e=(write p e1 (read p e))). -Proof. - intros Env A e p; eapply ex_intro. - autorewrite with placeeq. (* Here is the bug *) - auto. -Qed. - diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v index 85c09dbd..1845dd1f 100644 --- a/test-suite/bugs/opened/shouldnotfail/1501.v +++ b/test-suite/bugs/opened/shouldnotfail/1501.v @@ -8,7 +8,7 @@ Require Export Setoid. Section Essais. (* Parametrized Setoid *) -Parameter K : Type -> Type. +Parameter K : Type -> Type. Parameter equiv : forall A : Type, K A -> K A -> Prop. Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x. Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x. @@ -40,7 +40,7 @@ Parameter Hint Resolve equiv_refl equiv_sym equiv_trans: monad. -Add Relation K equiv +Add Relation K equiv reflexivity proved by (@equiv_refl) symmetry proved by (@equiv_sym) transitivity proved by (@equiv_trans) @@ -67,7 +67,7 @@ Proof. unfold fequiv; intros; eapply equiv_trans; auto with monad. Qed. -Add Relation (fun (A B:Type) => A -> K B) fequiv +Add Relation (fun (A B:Type) => A -> K B) fequiv reflexivity proved by (@fequiv_refl) symmetry proved by (@fequiv_sym) transitivity proved by (@fequiv_trans) @@ -82,12 +82,12 @@ Qed. Lemma test: forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> + (equiv m1 m2) -> (equiv m2 m3) -> equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) (bind m2 (fun a => bind m3 (fun a' => f a a'))). Proof. - intros A B m1 m2 m3 f H1 H2. + intros A B m1 m2 m3 f H1 H2. setoid_rewrite H1. (* this works *) setoid_rewrite H2. trivial by equiv_refl. -Qed. +Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v index 766bf524..de77e35d 100644 --- a/test-suite/bugs/opened/shouldnotfail/1596.v +++ b/test-suite/bugs/opened/shouldnotfail/1596.v @@ -11,12 +11,12 @@ Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with Definition t := (X.t * Y.t)%type. Definition t := (X.t * Y.t)%type. - Definition eq (xy1:t) (xy2:t) := + Definition eq (xy1:t) (xy2:t) := let (x1,y1) := xy1 in let (x2,y2) := xy2 in (X.eq x1 x2) /\ (Y.eq y1 y2). - Definition lt (xy1:t) (xy2:t) := + Definition lt (xy1:t) (xy2:t) := let (x1,y1) := xy1 in let (x2,y2) := xy2 in (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)). @@ -101,7 +101,7 @@ Definition t := (X.t * Y.t)%type. Defined. Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. End OrderedPair. Module MessageSpi. @@ -189,8 +189,8 @@ n)->(hedge_synthesis_relation h m n). Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message) (n:MessageSpi.message) {struct m} : bool := - if H.mem (m,n) h - then true + if H.mem (m,n) h + then true else false. Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation @@ -221,8 +221,8 @@ n). Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t) {struct m} : bool := - if H.mem (m,n) h - then true + if H.mem (m,n) h + then true else false. Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation @@ -235,7 +235,7 @@ n). induction m;simpl;intro. elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. apply SynInc;apply H.mem_2;trivial. - + rewrite H in H0. (* !! impossible here !! *) discriminate H0. Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v index 800c431e..d95c2108 100644 --- a/test-suite/bugs/opened/shouldnotfail/1671.v +++ b/test-suite/bugs/opened/shouldnotfail/1671.v @@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type := Variable P : forall bo, hdlist bo -> Prop. Variable all : forall bo l, P bo l. -Definition F (l:hdlist tt) : P tt l := +Definition F (l:hdlist tt) : P tt l := match l in hdlist u return P u l with | cons (cons l') => all tt _ end. |