Merge tag 'upstream/8.5_beta2+dfsg' into test

Upstream version 8.5~beta2+dfsg

1 files changed, 3 insertions, 9 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c8b9a208..5cc4c835 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