Merge branch 'v8.5'

11 files changed, 165 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/2602.v b/test-suite/bugs/closed/2602.v
new file mode 100644
index 000000000..f07447886
--- /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
diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
new file mode 100644
index 000000000..bb673f38c
--- /dev/null
+++ b/test-suite/bugs/closed/3210.v
@@ -0,0 +1,22 @@
+(* 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.
+
+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 *)
diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
new file mode 100644
index 000000000..d41d23173
--- /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.
diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v
index 29ee14873..02eca64ee 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
diff --git a/test-suite/bugs/opened/3467.v b/test-suite/bugs/closed/3467.v
index 900bfc34b..7e3711624 100644
--- a/test-suite/bugs/opened/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.
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
new file mode 100644
index 000000000..9125ab16d
--- /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).
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
new file mode 100644
index 000000000..06188e7b1
--- /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
diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/opened/2456.v
index 56f046c4d..6cca5c9fb 100644
--- a/test-suite/bugs/closed/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/closed/3593.v b/test-suite/bugs/opened/3593.v
index 25f9db6b2..d83b90060 100644
--- a/test-suite/bugs/closed/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.
diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/opened/3848.v
index b66aeccaf..9413daa04 100644
--- a/test-suite/bugs/closed/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 *)
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 4eb2dbe9f..ce9050d42 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.