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

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

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(-)

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

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

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 9fea58122001535bdee63317b56f2afb727167c7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 14:05:16 +0100
Subject: Somehow fixing bug #3467.

The notations using tactics in term seem now not to respect globalized names.
It is not obvious that this is the expected behaviour, but at least it does
not die with an anomaly.
---
 tactics/tacsubst.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 42e61cb57e..afffaffbe9 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -27,9 +27,8 @@ let subst_quantified_hypothesis _ x = x
 
 let subst_declared_or_quantified_hypothesis _ x = x
 
-let subst_glob_constr_and_expr subst (c,e) =
-  assert (Option.is_empty e); (* e<>None only for toplevel tactics *)
-  (Detyping.subst_glob_constr subst c,None)
+let subst_glob_constr_and_expr subst (c, e) =
+  (Detyping.subst_glob_constr subst c, e)
 
 let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
 
-- 
cgit v1.2.3


From f4d7d60b90ee03179479f8e3427bd1a5729135f2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 27 Feb 2015 15:43:06 +0100
Subject: Make coq_makefile generate double-colon rules for clean and
 archclean. (Fix bug #4080)

---
 tools/coq_makefile.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 84b4b5e5df..85206b8232 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -321,7 +321,7 @@ let make_makefile sds =
   end
 
 let clean sds sps =
-  print "clean:\n";
+  print "clean::\n";
   if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile || !some_mlpackfile then begin
     print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
     print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
@@ -343,7 +343,7 @@ let clean sds sps =
     (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n")
     sds;
   print "\n";
-  print "archclean:\n";
+  print "archclean::\n";
   print "\trm -f *.cmx *.o\n";
   List.iter
     (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n")
-- 
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(-)

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

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(-)

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 1388171a48d8e068d5d0ed93b74faa4ac7da5f7f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 14:23:02 +0100
Subject: Fixing typo resulting in wrong printing of return clauses for
 inductive types with let-in in arity.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index adf714db35..356a699c66 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -273,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let ind_tags =
-    rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+    rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
     Array.map2 (fun c n ->
       let d,_ = decompose_prod_assum c in
-- 
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).

---
 pretyping/cases.ml            | 27 ++++++++++++++++++++-------
 test-suite/bugs/closed/3210.v |  9 +++++++++
 test-suite/success/Case22.v   | 12 ++++++++++++
 3 files changed, 41 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/bugs/closed/3210.v

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7c3165fa8e..fcbe90b6a7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind =
    applist (mkIndU indu,List.rev evarl)
 
 let try_find_ind env sigma typ realnames =
-  let (IndType(_,realargs) as ind) = find_rectype env sigma typ in
+  let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in
   let names =
     match realnames with
       | Some names -> names
-      | None -> List.make (List.length realargs) Anonymous in
+      | None ->
+          let ind = fst (fst (dest_ind_family indf)) in
+          List.make (inductive_nrealdecls ind) Anonymous in
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind evdref env loc ty tyi =
@@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t)
 
 let recover_initial_subpattern_names = List.map2 set_declaration_name
 
-let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
+let recover_and_adjust_alias_names names sign =
+  let rec aux = function
+  | [],[] ->
+      []
+  | x::names, (_,None,t)::sign ->
+      (x,(alias_of_pat x,None,t)) :: aux (names,sign)
+  | names, (na,(Some _ as c),t)::sign ->
+      (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign)
+  | _ -> assert false
+  in
+  List.split (aux (names,sign))
 
 let push_rels_eqn sign eqn =
   {eqn with
@@ -1695,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t =
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
 	let sign = make_arity_signature env true indf' in
-	let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
-	let p = List.length realargs in
+        let patl = pat :: List.rev patl in
+	let patl,sign = recover_and_adjust_alias_names patl sign in
+	let p = List.length patl in
 	let env' = push_rel_context sign env in
-	let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
-	patl@pat::patl',acc_sign,acc
+	let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
+	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let d = (alias_of_pat pat,None,typ) in
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 5f8c0bfbb04de58a527d373c3994592e5853d4e2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 16:32:38 +0100
Subject: Hack so that refine_no_check accepts an argument which is a match on
 an inductive type with let-in in the arity (until logic.ml disappears).

---
 tactics/tactics.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ccf4795d68..ad6684e25b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1122,11 +1122,18 @@ let enforce_prop_bound_names rename tac =
   | _ ->
       tac
 
+let rec contract_letin_in_lam_header c =
+  match kind_of_term c with
+  | Lambda (x,t,c)  -> mkLambda (x,t,contract_letin_in_lam_header c)
+  | LetIn (x,b,t,c) -> contract_letin_in_lam_header (subst1 b c)
+  | _ -> c
+
 let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) 
     rename i (elim, elimty, bindings) indclause =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
+  let elim = contract_letin_in_lam_header elim in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
@@ -1280,6 +1287,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
+  let elim = contract_letin_in_lam_header elim in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
@@ -3656,6 +3664,7 @@ let induction_tac with_evars params indvars elim gl =
   let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
   let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
+  let elimc = contract_letin_in_lam_header elimc in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
   let elimclause =
     pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
-- 
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. *)
---
 kernel/inductive.ml           |  2 +-
 pretyping/inductiveops.ml     |  2 +-
 pretyping/reductionops.ml     | 13 +++++++++++++
 pretyping/reductionops.mli    |  1 +
 pretyping/retyping.ml         |  5 +++--
 test-suite/bugs/closed/3210.v | 13 +++++++++++++
 6 files changed, 32 insertions(+), 4 deletions(-)

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6b4dd536a1..ca814f497c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -364,7 +364,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
       let cstr = ith_constructor_of_inductive ind (i+1) in
       let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in
       vargs @ [dep_cstr] in
-    let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
+    let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base args in
   Array.mapi build_one_branch mip.mind_nf_lc
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 356a699c66..7f6a4a6442 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -526,7 +526,7 @@ let type_case_branches_with_names env indspec p c =
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
-  let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+  let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ec34383820..2c70a6c9a0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1628,3 +1628,16 @@ let head_unfold_under_prod ts env _ c =
 	    | Const cst -> beta_applist (unfold cst,l)
 	    | _ -> c in
   aux c
+
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | Evar ev, _ ->
+      (match safe_evar_value sigma ev with
+      | Some body -> stacklam n env body stack
+      | None -> applist (substl env t, stack))
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7c61d4e143..d4f061c5be 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -278,6 +278,7 @@ val whd_meta : evar_map -> constr -> constr
 val plain_instance : constr Metamap.t -> constr -> constr
 val instance : evar_map -> constr Metamap.t -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cd52ba44da..213d7ddda4 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma =
     | Ind ind -> rename_type_of_inductive env ind
     | Construct cstr -> rename_type_of_constructor env cstr
     | Case (_,p,c,lf) ->
-        let Inductiveops.IndType(_,realargs) =
+        let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
           with Not_found ->
@@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let t = whd_beta sigma (applist (p, realargs)) in
+        let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in
+        let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
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(-)

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 eb3e8efaaafd0de673184db85b9b647cfa24dd92 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Feb 2015 17:18:16 +0100
Subject: STM: Considering Stack_overflow as a normal tactic error (Close
 #3576)

---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 5edf480446..b38407c045 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1067,7 +1067,7 @@ end = struct (* {{{ *)
       ignore(Future.join checked_proof);
       RespBuiltProof(proof,time)
     with
-    | e when Errors.noncritical e ->
+    | e when Errors.noncritical e || e = Stack_overflow ->
         let (e, info) = Errors.push e in
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
-- 
cgit v1.2.3


From e43abf43a78a5bbeed720d50cd1ea68fdfc672f2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Feb 2015 17:27:12 +0100
Subject: simpl: honor Global for "simpl: never" (Close: 3206)

It was an integer overflow!  All sorts of memories.
---
 pretyping/reductionops.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2c70a6c9a0..09eb38bd12 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -64,7 +64,10 @@ module ReductionBehaviour = struct
         if Lib.is_in_section (ConstRef c) then
           let vars, _, _ = Lib.section_segment_of_constant c in
           let extra = List.length vars in
-          let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
+          let nargs' =
+             if b.b_nargs = max_int then max_int
+             else if b.b_nargs < 0 then b.b_nargs
+             else b.b_nargs + extra in
           let recargs' = List.map ((+) extra) b.b_recargs in
           { b with b_nargs = nargs'; b_recargs = recargs' }
         else b
-- 
cgit v1.2.3


From 9f09cbfe36c38a97644ea98c5497636fe74d98d6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 18:59:59 +0100
Subject: Taking current env and not global env in b286c9f4f42f (4 commits ago,
 as revealed by #2141).

---
 pretyping/retyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 213d7ddda4..a56861c683 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -109,7 +109,7 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in
+        let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
         let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
-- 
cgit v1.2.3


From 64a139406409084f25d3ce35e0fa71bbccc63a20 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 20:26:33 +0100
Subject: Fixing bug #3249.

Instead of substituting carelessly the recursive names in Ltac interpretation,
we declare them in the environment beforehand, so that they get globalized
as themselves. We restore the environment afterwards by transactifying the
globalization procedure.
---
 toplevel/vernacentries.ml | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a2d2e3d91c..15d57d20f1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -960,20 +960,27 @@ let register_ltac local isrec tacl =
     (name, body)
   in
   let rfun = List.map map tacl in
-  let ltacrecvars =
+  let recvars =
     let fold accu (op, _) = match op with
     | UpdateTac _ -> accu
-    | NewTac id -> Id.Map.add id (Lib.make_kn id) accu
+    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
     in
-    if isrec then List.fold_left fold Id.Map.empty rfun
-    else Id.Map.empty
+    if isrec then List.fold_left fold [] rfun
+    else []
   in
-  let ist = { (Tacintern.make_empty_glob_sign ()) with Genintern.ltacrecvars; } in
+  let ist = Tacintern.make_empty_glob_sign () in
   let map (name, body) =
     let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
     (name, body)
   in
-  let defs = List.map map rfun in
+  let defs () =
+    (** Register locally the tactic to handle recursivity. This function affects
+        the whole environment, so that we transactify it afterwards. *)
+    let iter_rec (sp, kn) = Nametab.push_tactic (Until 1) sp kn in
+    let () = List.iter iter_rec recvars in
+    List.map map rfun
+  in
+  let defs = Future.transactify defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
     Tacenv.register_ltac false local id tac;
-- 
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

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 46969b0ece809598b4dd35c688a8ba5237b01efd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 20:40:58 +0100
Subject: Fixing OCaml 3.12 compilation.

---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 15d57d20f1..1b8fdd8aed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -976,7 +976,7 @@ let register_ltac local isrec tacl =
   let defs () =
     (** Register locally the tactic to handle recursivity. This function affects
         the whole environment, so that we transactify it afterwards. *)
-    let iter_rec (sp, kn) = Nametab.push_tactic (Until 1) sp kn in
+    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
     let () = List.iter iter_rec recvars in
     List.map map rfun
   in
-- 
cgit v1.2.3


From fc1b3ef9d7270938cd83c524aae0383093b7a4b5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 20:42:44 +0100
Subject: Removing the unused field ltacrecvars of tactic internalization.

---
 interp/constrintern.ml                |  1 -
 interp/genintern.ml                   |  1 -
 interp/genintern.mli                  |  1 -
 plugins/decl_mode/decl_proof_instr.ml |  2 +-
 tactics/tacintern.ml                  | 12 +++---------
 tactics/tacintern.mli                 |  1 -
 tactics/tacinterp.ml                  |  6 ++----
 7 files changed, 6 insertions(+), 18 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 68f0050d4d..5151d2a10a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1567,7 +1567,6 @@ let internalize globalenv env allow_patvar lvar c =
           let lvars = Id.Set.union lvars env.ids in
           let ist = {
             Genintern.ltacvars = lvars;
-            ltacrecvars = Id.Map.empty;
             genv = globalenv;
           } in
           let (_, glb) = Genintern.generic_intern ist gen in
diff --git a/interp/genintern.ml b/interp/genintern.ml
index c78b13a8f5..7795946d56 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -12,7 +12,6 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   genv : Environ.env }
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 6e63f71c5d..28f4f530b2 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -12,7 +12,6 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   genv : Environ.env }
 
 (** {5 Internalization functions} *)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d25681dcf..c61079e636 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1454,7 +1454,7 @@ let do_instr raw_instr pts =
             let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma; } in
       let env=  pf_env gl in
-      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in
+      let ist = {ltacvars = Id.Set.empty; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) env sigma glob_instr in
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c8b9a2084c..5cc4c835bc 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -48,12 +48,10 @@ let error_tactic_expected loc =
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  ltacrecvars : ltac_constant Id.Map.t;
-     (* ltac recursive names *)
   genv : Environ.env }
 
 let fully_empty_glob_sign =
-  { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env }
+  { ltacvars = Id.Set.empty; genv = Environ.empty_env }
 
 let make_empty_glob_sign () =
   { fully_empty_glob_sign with genv = Global.env () }
@@ -64,8 +62,6 @@ let find_ident id ist =
   Id.Set.mem id ist.ltacvars ||
   Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
-let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars
-
 (* a "var" is a ltac var or a var introduced by an intro tactic *)
 let find_var id ist = Id.Set.mem id ist.ltacvars
 
@@ -116,9 +112,7 @@ let intern_ltac_variable ist = function
       if find_var id ist then
 	(* A local variable of any type *)
 	ArgVar (loc,id)
-      else
-      (* A recursive variable *)
-      ArgArg (loc,find_recvar id ist)
+      else raise Not_found
   | _ ->
       raise Not_found
 
@@ -801,7 +795,7 @@ let glob_tactic_env l env x =
     List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
   (intern_pure_tactic
-    { ltacvars; ltacrecvars = Id.Map.empty; genv = env })
+    { ltacvars; genv = env })
     x
 
 let split_ltac_fun = function
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 2e662e5823..a6e28d568d 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -19,7 +19,6 @@ open Nametab
 
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : ltac_constant Id.Map.t;
   genv : Environ.env }
 
 val fully_empty_glob_sign : glob_sign
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index af541b8b9e..8826875a38 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2251,8 +2251,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
     (intern_pure_tactic {
-      ltacvars; ltacrecvars = Id.Map.empty;
-      genv = env } t)
+      ltacvars; genv = env } t)
   end
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -2262,8 +2261,7 @@ let _ = Proof_global.set_interp_tac interp
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
   let hide_interp env =
-    let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
-                genv = env } in
+    let ist = { ltacvars = Id.Set.empty; genv = env } in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with
-- 
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

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