Merge branch 'v8.5'

29 files changed, 242 insertions, 52 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/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/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/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/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index adf714db35..7f6a4a6442 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
@@ -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..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
@@ -1628,3 +1631,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..a56861c683 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_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]))
           | _ -> t)
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 *)
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
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 *)
 
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
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
diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
new file mode 100644
index 0000000000..bb673f38c2
--- /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 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.
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
diff --git a/test-suite/bugs/opened/3467.v b/test-suite/bugs/closed/3467.v
index 900bfc34b3..7e37116249 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 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).
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
diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/opened/2456.v
index 56f046c4d7..6cca5c9fba 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 25f9db6b28..d83b900607 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 b66aeccaff..9413daa041 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 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.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f9a84887d9..93df848de4 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")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a2d2e3d91c..1b8fdd8aed 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 (Nametab.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;