Merge branch 'v8.5'

5 files changed, 16 insertions, 17 deletions

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