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/constrintern.ml | |
| parent | 46969b0ece809598b4dd35c688a8ba5237b01efd (diff) | |
Removing the unused field ltacrecvars of tactic internalization.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 1 |
1 files changed, 0 insertions, 1 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 |