diff options
| author | Pierre-Marie Pédrot | 2016-11-30 23:08:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-03 20:05:57 +0200 |
| commit | 9262f440e8d8b8559c5488b1333c023f7305d811 (patch) | |
| tree | f09ec49bd38357d949876ca4e494fe22ff2b6a0c /interp/genintern.mli | |
| parent | 267c880c5e8b73770316518a2a820e779c121fdb (diff) | |
Allowing to pass arbitrary data in internalization environments.
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 4b0354be39..658caa08c2 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} *) |