diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:08:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:13:22 +0100 |
| commit | 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch) | |
| tree | d70ab7e108af307cbd9e996b78e0f9f5e945aa42 /interp/genintern.mli | |
| parent | fb59652405d0e6a9d1100142d473374cd82ae16b (diff) | |
Removing the need of evarmaps in constr internalization.
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
Diffstat (limited to 'interp/genintern.mli')
| -rw-r--r-- | interp/genintern.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/genintern.mli b/interp/genintern.mli index 7027315e7..970f27f66 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -13,7 +13,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; ltacrecvars : Nametab.ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } (** {5 Internalization functions} *) |