From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- test-suite/output/inference.out | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 576fbd7c0b..c0eede99e6 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n : T n in ?y ?y0 : T n +fun n : nat => let x := A n : T n in ?t ?y : T n : forall n : nat, T n where -?y : [n : nat x := A n : T n |- ?T -> T n] -?y0 : [n : nat x := A n : T n |- ?T] -fun n : nat => ?y ?y0 : T n +?t : [n : nat x := A n : T n |- ?T -> T n] +?y : [n : nat x := A n : T n |- ?T] +fun n : nat => ?t ?y : T n : forall n : nat, T n where -?y : [n : nat |- ?T -> T n] -?y0 : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?y : [n : nat |- ?T] -- cgit v1.2.3 From 5db9588098f9f02d923c21f3914e3c671b10728f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Jan 2017 13:07:11 +0100 Subject: Quick hack to fix interpretation of patterns in Ltac. Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip through the pretyper, and relies on suspicious flagging of evars in the evar source field to recognize original pattern holes. After the pattern_of_constr function was made evar-insensitive, it expanded evars that were solved by magical side-effects of the pretyper, even if it hadn't been asked to perform any heuristics. We backtrack on the insensitivity of the pattern_of_constr function. This may have a performance penalty in other dubious code, e.g. hints. In the long run we should get rid of the pattern_of_constr function. --- test-suite/success/change_pattern.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 test-suite/success/change_pattern.v (limited to 'test-suite') diff --git a/test-suite/success/change_pattern.v b/test-suite/success/change_pattern.v new file mode 100644 index 0000000000..874abf49f1 --- /dev/null +++ b/test-suite/success/change_pattern.v @@ -0,0 +1,34 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Axiom vector : Type -> nat -> Type. + +Record KleeneStore i j a := kleeneStore + { dim : nat + ; peek : vector j dim -> a + ; pos : vector i dim + }. + +Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b := + kleeneStore (fun v => f (peek v)) (pos s). + +Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg + { coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }. + +Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x). +Axiom t : Type -> Type. +Axiom traverse : KleeneCoalg (fun x => x) t. + +Definition size a (x:t a) : nat := dim (traverse a a x). + +Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False. +Proof. +destruct y. +pose (X := KSmap (traverse a unit) (traverse unit a x)). +set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))). +clearbody e. +(** The pattern generated by change must have holes where there were implicit + arguments in the original user-provided term. This particular example fails + if this is not the case because the inferred argument does not coincide with + the one in the considered term. *) +progress (change (dim (traverse unit a x)) with (dim X) in e). -- cgit v1.2.3 From d331543b7b759bb97ea1ece32501cd0149627e9f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Apr 2017 16:37:11 +0200 Subject: Adding a test for the correctness of normalization in legacy typeclasses. This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b. --- test-suite/success/old_typeclass.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test-suite/success/old_typeclass.v (limited to 'test-suite') diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v new file mode 100644 index 0000000000..01e35810b0 --- /dev/null +++ b/test-suite/success/old_typeclass.v @@ -0,0 +1,13 @@ +Require Import Setoid Coq.Classes.Morphisms. +Set Typeclasses Legacy Resolution. + +Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. + +Axiom In : Prop. +Axiom union_spec : In <-> True. + +Lemma foo : In /\ True. +Proof. +progress rewrite union_spec. +repeat constructor. +Qed. -- cgit v1.2.3 From 2e6a89238dc7197057d0da80a16f4b4b1e41bfd8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Apr 2017 18:35:18 +0200 Subject: Adding a test for 'rewrite in *' when an evar is solved by side-effect. --- test-suite/success/rewrite_evar.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 test-suite/success/rewrite_evar.v (limited to 'test-suite') diff --git a/test-suite/success/rewrite_evar.v b/test-suite/success/rewrite_evar.v new file mode 100644 index 0000000000..f7ad261cbb --- /dev/null +++ b/test-suite/success/rewrite_evar.v @@ -0,0 +1,8 @@ +Require Import Coq.Setoids.Setoid. + +Goal forall (T2 MT1 MT2 : Type) (x : T2) (M2 m2 : MT2) (M1 m1 : MT1) (F : T2 -> MT1 -> MT2 -> Prop), + (forall (defaultB : T2) (m3 : MT1) (m4 : MT2), F defaultB m3 m4 <-> True) -> F x M1 M2 -> F x m1 m2. + intros ????????? H' H. + rewrite (H' _) in *. + (** The above rewrite should also rewrite in H. *) + Fail progress rewrite H' in H. -- cgit v1.2.3