Removing the unused field ltacrecvars of tactic internalization.

3 files changed, 5 insertions, 14 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