diff options
Diffstat (limited to 'interp/genintern.mli')
| -rw-r--r-- | interp/genintern.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b0354be3..658caa08c 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -10,9 +10,15 @@ open Names open Mod_subst open Genarg +module Store : Store.S + type glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Store.t; +} + +val empty_glob_sign : Environ.env -> glob_sign (** {5 Internalization functions} *) |