From f65aac12bb8b2071dcc15f5351194c649d3f7196 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 21:57:51 +0100
Subject: Test for #2602, which seems now fixed.

---
 test-suite/bugs/closed/2602.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/2602.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2602.v b/test-suite/bugs/closed/2602.v
new file mode 100644
index 0000000000..f074478868
--- /dev/null
+++ b/test-suite/bugs/closed/2602.v
@@ -0,0 +1,8 @@
+Goal exists m, S m > 0.
+eexists.
+match goal with
+ | |- context [ S ?a ] =>
+     match goal with
+       | |- S a > 0 => idtac
+     end
+end.
\ No newline at end of file
-- 
cgit v1.2.3


From 321249f0ccc9b7b6fedbab411fac4aa443e0dd43 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 13:25:11 +0100
Subject: Moving test of #3848 to "opened".

---
 test-suite/bugs/closed/3848.v | 21 ---------------------
 test-suite/bugs/opened/3848.v | 21 +++++++++++++++++++++
 2 files changed, 21 insertions(+), 21 deletions(-)
 delete mode 100644 test-suite/bugs/closed/3848.v
 create mode 100644 test-suite/bugs/opened/3848.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v
deleted file mode 100644
index b66aeccaff..0000000000
--- a/test-suite/bugs/closed/3848.v
+++ /dev/null
@@ -1,21 +0,0 @@
-Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
-Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
-Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
-Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
-Arguments eisretr {A B} f {_} _.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
-Generalizable Variables A B f g e n.
-Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
-           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
-: (forall a:A, P a) -> (forall b:B, Q b).
-  admit.
-Defined.
-
-Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
-      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
-: (forall b : B, Q b) -> forall a : A, P a.
-Proof.
-  refine (functor_forall
-            (f^-1)
-            (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
-Defined. (* Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
new file mode 100644
index 0000000000..b66aeccaff
--- /dev/null
+++ b/test-suite/bugs/opened/3848.v
@@ -0,0 +1,21 @@
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Generalizable Variables A B f g e n.
+Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
+           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
+: (forall a:A, P a) -> (forall b:B, Q b).
+  admit.
+Defined.
+
+Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
+      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
+: (forall b : B, Q b) -> forall a : A, P a.
+Proof.
+  refine (functor_forall
+            (f^-1)
+            (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
+Defined. (* Error: Attempt to save an incomplete proof *)
-- 
cgit v1.2.3


From 525c934044714eb99ca824e5dc929b518aae3730 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 13:25:36 +0100
Subject: Made test for #3392 rely less on unification.

---
 test-suite/bugs/closed/3392.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v
index 29ee148733..02eca64eea 100644
--- a/test-suite/bugs/closed/3392.v
+++ b/test-suite/bugs/closed/3392.v
@@ -24,9 +24,8 @@ Proof.
   intros.
   refine (isequiv_adjointify (functor_forall f g)
                              (functor_forall (f^-1)
-                                             (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y
-                             )) _ _); 
-  intros h.
+                                             (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f H x # (g (f^-1 x))^-1 y
+                             )) _ _); intros h.
   - abstract (
         apply path_forall; intros b; unfold functor_forall;
         rewrite eisadj;
@@ -37,4 +36,4 @@ Proof.
         rewrite eissect;
         apply apD
       ).
-Defined.
+Defined.
\ No newline at end of file
-- 
cgit v1.2.3


From 7012d65f71752a89cded69d6c2e7045f3a7cadde Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 13:29:11 +0100
Subject: Moving tests for #2456 and #3593 to "opened" until they're fixed.

---
 test-suite/bugs/closed/2456.v | 53 -------------------------------------------
 test-suite/bugs/closed/3593.v | 10 --------
 test-suite/bugs/opened/2456.v | 53 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/3593.v | 10 ++++++++
 4 files changed, 63 insertions(+), 63 deletions(-)
 delete mode 100644 test-suite/bugs/closed/2456.v
 delete mode 100644 test-suite/bugs/closed/3593.v
 create mode 100644 test-suite/bugs/opened/2456.v
 create mode 100644 test-suite/bugs/opened/3593.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v
deleted file mode 100644
index 56f046c4d7..0000000000
--- a/test-suite/bugs/closed/2456.v
+++ /dev/null
@@ -1,53 +0,0 @@
-
-Require Import Equality.
-
-Parameter Patch : nat -> nat -> Set.
-
-Inductive Catch (from to : nat) : Type
-    := MkCatch : forall (p : Patch from to),
-                 Catch from to.
-Implicit Arguments MkCatch [from to].
-
-Inductive CatchCommute5
-        : forall {from mid1 mid2 to : nat},
-          Catch from mid1
-       -> Catch mid1 to
-       -> Catch from mid2
-       -> Catch mid2 to
-       -> Prop
-     := MkCatchCommute5 :
-           forall {from mid1 mid2 to : nat}
-                  (p : Patch from mid1)
-                  (q : Patch mid1 to)
-                  (q' : Patch from mid2)
-                  (p' : Patch mid2 to),
-           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
-
-Inductive CatchCommute {from mid1 mid2 to : nat}
-                       (p : Catch from mid1)
-                       (q : Catch mid1 to)
-                       (q' : Catch from mid2)
-                       (p' : Catch mid2 to)
-                     : Prop
-    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
-                         CatchCommute p q q' p'.
-Notation "<< p , q >> <~> << q' , p' >>"
-    := (CatchCommute p q q' p')
-    (at level 60, no associativity).
-
-Lemma CatchCommuteUnique2 :
-      forall {from mid mid' to : nat}
-             {p   : Catch from mid}  {q   : Catch mid  to}
-             {q'  : Catch from mid'} {p'  : Catch mid' to}
-             {q'' : Catch from mid'} {p'' : Catch mid' to}
-             (commute1 : <<p, q>> <~> <<q', p'>>)
-             (commute2 : <<p, q>> <~> <<q'', p''>>),
-      (p' = p'') /\ (q' = q'').
-Proof with auto.
-intros.
-set (X := commute2).
-dependent destruction commute1;
-dependent destruction catchCommuteDetails;
-dependent destruction commute2;
-dependent destruction catchCommuteDetails generalizing X.
-Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v
deleted file mode 100644
index 25f9db6b28..0000000000
--- a/test-suite/bugs/closed/3593.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Set Universe Polymorphism.
-Set Printing All.
-Set Implicit Arguments.
-Record prod A B := pair { fst : A ; snd : B }.
-Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
-simpl; intros.
-  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). 
-  reflexivity.
-Qed.
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
new file mode 100644
index 0000000000..56f046c4d7
--- /dev/null
+++ b/test-suite/bugs/opened/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v
new file mode 100644
index 0000000000..25f9db6b28
--- /dev/null
+++ b/test-suite/bugs/opened/3593.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+Set Printing All.
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
+simpl; intros.
+  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
+  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). 
+  reflexivity.
+Qed.
-- 
cgit v1.2.3


From dbdf0648f4588d812a20ea4ba7d3e866f024073c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 14:01:41 +0100
Subject: Add test-suite file for #3649.

---
 test-suite/bugs/closed/3649.v | 57 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 test-suite/bugs/closed/3649.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
new file mode 100644
index 0000000000..06188e7b1b
--- /dev/null
+++ b/test-suite/bugs/closed/3649.v
@@ -0,0 +1,57 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y" (at level 70, no associativity).
+Open Scope type_scope.
+Axiom admit : forall {T}, T.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Reserved Infix "o" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac.
+Global Set Primitive Projections.
+Delimit Scope morphism_scope with morphism.
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+
+    identity : forall x, morphism x x;
+    compose : forall s d d',
+                morphism d d'
+                -> morphism s d
+                -> morphism s d'
+    where "f 'o' g" := (compose f g) }.
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d
+                              -> morphism D (object_of s) (object_of d) }.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
+  { morphism_inverse : morphism C d s }.
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+Definition composeT C D (F F' F'' : Functor C D) (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
+: NaturalTransformation F F''.
+  exact admit.
+Defined.
+Definition functor_category (C D : PreCategory) : PreCategory.
+  exact (@Build_PreCategory (Functor C D)
+                            (@NaturalTransformation C D)
+                            admit
+                            (@composeT C D)).
+Defined.
+Goal forall (C D : PreCategory) (G G' : Functor C D)
+            (T : @NaturalTransformation C D G G')
+            (H : @IsIsomorphism (@functor_category C D) G G' T)
+            (x : C),
+       @paths (morphism D (G x) (G x))
+              (@compose D (G x) (G' x) (G x)
+                        ((@morphism_inverse (@functor_category C D) G G' T H) x)
+                        (T x)) (@identity D (G x)).
+  intros.
+  (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
+  let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
+  let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
+  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file
-- 
cgit v1.2.3


From 3248466ca57b5121e5a29bf6fd6619c512a52349 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 16:23:36 +0100
Subject: Fix test-suite files for bugs #2456 and #3593, still open.

---
 test-suite/bugs/opened/2456.v | 4 ++--
 test-suite/bugs/opened/3593.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
index 56f046c4d7..6cca5c9fba 100644
--- a/test-suite/bugs/opened/2456.v
+++ b/test-suite/bugs/opened/2456.v
@@ -46,8 +46,8 @@ Lemma CatchCommuteUnique2 :
 Proof with auto.
 intros.
 set (X := commute2).
-dependent destruction commute1;
+Fail dependent destruction commute1;
 dependent destruction catchCommuteDetails;
 dependent destruction commute2;
 dependent destruction catchCommuteDetails generalizing X.
-Admitted.
\ No newline at end of file
+Admitted.
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v
index 25f9db6b28..d83b900607 100644
--- a/test-suite/bugs/opened/3593.v
+++ b/test-suite/bugs/opened/3593.v
@@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }.
 Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
 simpl; intros.
   constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). 
+  Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
   reflexivity.
 Qed.
-- 
cgit v1.2.3


From 926fcf01baecd01c2e46d17a31077b942d01971d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 16:46:41 +0100
Subject: Moving test for #3467 to closed after PMP's fix.

---
 test-suite/bugs/closed/3467.v | 6 ++++++
 test-suite/bugs/opened/3467.v | 6 ------
 2 files changed, 6 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/3467.v
 delete mode 100644 test-suite/bugs/opened/3467.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v
new file mode 100644
index 0000000000..900bfc34b3
--- /dev/null
+++ b/test-suite/bugs/closed/3467.v
@@ -0,0 +1,6 @@
+Module foo.
+  Notation x := $(exact I)$.
+End foo.
+Module bar.
+  Fail Include foo.
+End bar.
diff --git a/test-suite/bugs/opened/3467.v b/test-suite/bugs/opened/3467.v
deleted file mode 100644
index 900bfc34b3..0000000000
--- a/test-suite/bugs/opened/3467.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Module foo.
-  Notation x := $(exact I)$.
-End foo.
-Module bar.
-  Fail Include foo.
-End bar.
-- 
cgit v1.2.3


From 1019a654a8262ee1b8b1e1a7f652a7e3d111d20e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 16:47:43 +0100
Subject: Fix test for #3848, still open.

---
 test-suite/bugs/opened/3848.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
index b66aeccaff..9413daa041 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/opened/3848.v
@@ -18,4 +18,4 @@ Proof.
   refine (functor_forall
             (f^-1)
             (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
-Defined. (* Error: Attempt to save an incomplete proof *)
+Fail Defined. (* Error: Attempt to save an incomplete proof *)
-- 
cgit v1.2.3


From 172388eab4f34da71d82c4fab269bd6426c73853 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 14:24:19 +0100
Subject: Fixing first part of bug #3210 (inference of pattern-matching return
 clause in the presence of let-ins in the arity of inductive type).

---
 test-suite/bugs/closed/3210.v |  9 +++++++++
 test-suite/success/Case22.v   | 12 ++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/3210.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
new file mode 100644
index 0000000000..e66bf922d7
--- /dev/null
+++ b/test-suite/bugs/closed/3210.v
@@ -0,0 +1,9 @@
+(* Test support of let-in in arity of inductive types *)
+
+Inductive Foo : let X := Set in X :=
+| I : Foo.
+
+Definition foo (x : Foo) : bool :=
+  match x with
+  I => true
+  end.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 4eb2dbe9f5..ce9050d421 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -5,3 +5,15 @@ Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl
 intro.
 match goal with |- ?c => let x := eval cbv in c in change x end.
 Abort.
+
+Check forall x:I eq_refl, match x in I x return x = x with C => eq_refl end = eq_refl.
+
+(* This is bug #3210 *)
+
+Inductive I' : let X := Set in X :=
+| C' : I'.
+
+Definition foo (x : I') : bool :=
+  match x with
+  C' => true
+  end.
-- 
cgit v1.2.3


From b286c9f4f42febfd37f9715d81eaf118ab24aa94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 16:29:28 +0100
Subject: Add support so that the type of a match in an inductive type with
 let-in is reduced as if without let-in, when applied to arguments.

This allows e.g. to have a head-betazeta-reduced goal in the following example.

Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
---
 test-suite/bugs/closed/3210.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
index e66bf922d7..bb673f38c2 100644
--- a/test-suite/bugs/closed/3210.v
+++ b/test-suite/bugs/closed/3210.v
@@ -7,3 +7,16 @@ Definition foo (x : Foo) : bool :=
   match x with
   I => true
   end.
+
+Definition foo' (x : Foo) : x = x.
+case x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+elim x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+induction x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+destruct x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
-- 
cgit v1.2.3


From b3c66b03da5e7f3335960eb38a37f5f85f84119b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 17:12:40 +0100
Subject: Fix test for #3467, I had moved it in a dumb way.

---
 test-suite/bugs/closed/3467.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v
index 900bfc34b3..7e37116249 100644
--- a/test-suite/bugs/closed/3467.v
+++ b/test-suite/bugs/closed/3467.v
@@ -2,5 +2,5 @@ Module foo.
   Notation x := $(exact I)$.
 End foo.
 Module bar.
-  Fail Include foo.
+  Include foo.
 End bar.
-- 
cgit v1.2.3


From d7c8d18cca8a41db7ba12c8f6131e8a42491e962 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 20:36:19 +0100
Subject: Test for bug #3249.

---
 test-suite/bugs/closed/3249.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/3249.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
new file mode 100644
index 0000000000..d41d231739
--- /dev/null
+++ b/test-suite/bugs/closed/3249.v
@@ -0,0 +1,11 @@
+Set Implicit Arguments.
+
+Ltac ret_and_left T :=
+  let t := type of T in
+  lazymatch eval hnf in t with
+    | ?a /\ ?b => constr:(proj1 T)
+    | forall x : ?T', @?f x =>
+      constr:(fun x : T' => $(let fx := constr:(T x) in
+                              let t := ret_and_left fx in
+                              exact t)$)
+  end.
-- 
cgit v1.2.3


From 78d1a61730886f89b01fa4245e58b54dd50fb4cf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 21:10:30 +0100
Subject: Adding a test for bug #3612.

---
 test-suite/bugs/closed/3612.v | 47 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 test-suite/bugs/closed/3612.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
new file mode 100644
index 0000000000..9125ab16dd
--- /dev/null
+++ b/test-suite/bugs/closed/3612.v
@@ -0,0 +1,47 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \
+lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (580b25e05c7cc9e7a31430b3d9edb14ae12b7598) *)
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y  :>  T" (at level 70, y at next level, no associativity).
+Reserved Notation "x = y" (at level 70, no associativity).
+Open Scope type_scope.
+Global Set Universe Polymorphism.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Generalizable All Variables.
+Local Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} _ / .
+Arguments projT2 {A P} _ / .
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y .
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Local Open Scope path_scope.
+Axiom pr1_path : forall `{P : A -> Type} {u v : sigT P} (p : u = v), u.1 = v.1.
+Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope.
+Axiom pr2_path : forall `{P : A -> Type} {u v : sigT P} (p : u = v), p..1 # u.2 = v.2.
+Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope.
+Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (r : p..1 = q..1)
+           (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
+p = q.
+Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
+            (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
+       @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
+              (@idpath (@sigT A (fun x0 : A => B x0)) x).
+  intros A B x xx.
+  Set Printing All.
+  change (fun x => B x) with B in xx.
+  pose (path_path_sigma B x x xx) as x''.
+  clear x''.
+  Check (path_path_sigma B x x xx).
-- 
cgit v1.2.3