From 009718d9d0130a967261ae5d2484985522fc2f7c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 10 Oct 2016 10:58:09 +0200 Subject: Add test file for #4416. --- test-suite/bugs/closed/4416.v | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test-suite/bugs/closed/4416.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v new file mode 100644 index 0000000000..b97a8ce640 --- /dev/null +++ b/test-suite/bugs/closed/4416.v @@ -0,0 +1,3 @@ +Goal exists x, x. +unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. +(* Error: Incorrect number of goals (expected 2 tactics). *) \ No newline at end of file -- cgit v1.2.3 From b247761476c4b36f0945c19c23c171ea57701178 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 18:02:25 +0200 Subject: Fix for bug #4863, update the Proofview's env with side_effects. Partial solution to the handling of side effects in proofview. --- test-suite/bugs/closed/4863.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 test-suite/bugs/closed/4863.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v new file mode 100644 index 0000000000..e884355fde --- /dev/null +++ b/test-suite/bugs/closed/4863.v @@ -0,0 +1,32 @@ +Require Import Classes.DecidableClass. + +Inductive Foo : Set := +| foo1 | foo2. + +Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Proof. + intros P H. + refine (Build_Decidable _ (if H then true else false) _). + intuition congruence. +Qed. + +Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances. + +Goal forall (a b : Foo), {a=b}+{a<>b}. +intros. +abstract (abstract (decide equality)). (*abstract works here*) +Qed. + +Check ltac:(abstract (exact I)) : True. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. typeclasses eauto. typeclasses eauto. Qed. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. +refine _. +refine _. +Defined. +(*fails*) -- cgit v1.2.3 From af3538f0c6decdccd47abcdeb7b7eeaff64b69b5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 11 Oct 2016 12:40:31 +0200 Subject: Reverting generalization and cleaning of the return clause inference in v8.6. The move to systematically trying small inversion first bumps sometimes as feared to the weakness of unification (see #5107). ---- Revert "Posssible abstractions over goal variables when inferring match return clause." This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94. Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given." This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548. Revert "Trying a no-inversion no-dependency heuristic for match return clause." This reverts commit 2422aeb2b59229891508f35890653a9737988c00. --- test-suite/success/Case13.v | 38 -------------------------------------- 1 file changed, 38 deletions(-) (limited to 'test-suite') diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index 356a67efec..8f95484cfd 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -87,41 +87,3 @@ Check fun (x : E) => match x with c => e c end. Inductive C' : bool -> Set := c' : C' true. Inductive E' (b : bool) : Set := e' :> C' b -> E' b. Check fun (x : E' true) => match x with c' => e' true c' end. - -(* Check use of the no-dependency strategy when a type constraint is - given (and when the "inversion-and-dependencies-as-evars" strategy - is not strong enough because of a constructor with a type whose - pattern structure is not refined enough for it to be captured by - the inversion predicate) *) - -Inductive K : bool -> bool -> Type := F : K true true | G x : K x x. - -Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) => - match y with - | F => f y H1 - | G _ => f y H2 - end : Q y z. - -(* Check use of the maximal-dependency-in-variable strategy even when - no explicit type constraint is given (and when the - "inversion-and-dependencies-as-evars" strategy is not strong enough - because of a constructor with a type whose pattern structure is not - refined enough for it to be captured by the inversion predicate) *) - -Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) => - match y with - | F => f y true H1 - | G b => f y b H2 - end. - -(* Check use of the maximal-dependency-in-variable strategy for "Var" - variables *) - -Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z. -intros z P Q y H1 H2 f. -Show. -refine (match y with - | F => f y true H1 - | G b => f y b H2 - end). -Qed. -- cgit v1.2.3 From d226adf01f20ea946bbeac4d4c5cde75a4d77f32 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 11 Oct 2016 11:57:46 +0200 Subject: Fix bug #5123: mark all shelved evars unresolvable Previously, some splipped through and were caught by unrelated calls to typeclass resolution. --- test-suite/bugs/closed/5123.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 test-suite/bugs/closed/5123.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 0000000000..c171a10d10 --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,31 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) +Abort. \ No newline at end of file -- cgit v1.2.3 From 2bcae5b7a22019718973f65cafd271f735d3d85b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 11 Oct 2016 16:33:26 +0200 Subject: Fix test-suite file 5123 to fail in case of regression --- test-suite/bugs/closed/5123.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v index c171a10d10..bcde510ee6 100644 --- a/test-suite/bugs/closed/5123.v +++ b/test-suite/bugs/closed/5123.v @@ -21,6 +21,7 @@ Goal True. unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. all:cycle 2. eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. Abort. Goal True. @@ -28,4 +29,5 @@ Goal True. Unshelve. all:cycle 3. eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. Abort. \ No newline at end of file -- cgit v1.2.3 From 5dd690ee5975262d34d8dcc44191138c8d326f65 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 16 Jul 2016 16:24:59 +0200 Subject: Fixing a collision about the meta-variable ".." in recursive notations. This happens when recursive notations are used to define recursive notations. --- test-suite/success/Notations.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index b72a067407..2f7c62972a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l). Notation "'intros' x" := (S x) (at level 0). Goal True -> True. intros H. exact H. Qed. + +(* Check absence of collision on ".." in nested notations with ".." *) +Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). -- cgit v1.2.3