diff options
| author | Pierre-Marie Pédrot | 2015-02-28 00:58:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-28 00:58:29 +0100 |
| commit | fcd7926fa8bddc86f66e936ad0bf615326b8cb6d (patch) | |
| tree | fb1be444a7b66b253e27c93b23eb229aacee0645 /interp | |
| parent | 2206b405c19940ca4ded2179d371c21fd13f1b6b (diff) | |
| parent | 78d1a61730886f89b01fa4245e58b54dd50fb4cf (diff) | |
Merge branch 'v8.5'
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} *) |