diff options
| author | Pierre-Marie Pédrot | 2015-02-27 20:42:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-27 20:45:06 +0100 |
| commit | fc1b3ef9d7270938cd83c524aae0383093b7a4b5 (patch) | |
| tree | 9730c1cb313c2b9a510a5030291292353cd41331 /interp | |
| parent | 46969b0ece809598b4dd35c688a8ba5237b01efd (diff) | |
Removing the unused field ltacrecvars of tactic internalization.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 1 | ||||
| -rw-r--r-- | interp/genintern.ml | 1 | ||||
| -rw-r--r-- | interp/genintern.mli | 1 |
3 files changed, 0 insertions, 3 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} *) |