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 -
 3 files changed, 3 deletions(-)

(limited to 'interp')

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} *)
-- 
cgit v1.2.3