diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index f634719f9a..b6b6b48287 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -14,14 +14,20 @@ open Declarations (** The type of environments. *) +type link_info = + | Linked of string * bool + | LinkedInteractive of string * bool + | NotLinked type key = int option ref -type constant_key = constant_body * key +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; - env_inductives : mutual_inductive_body Mindmap_env.t; + env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -77,5 +83,5 @@ val lookup_constant_key : constant -> env -> constant_key val lookup_constant : constant -> env -> constant_body (** Mutual Inductives *) +val lookup_mind_key : mutual_inductive -> env -> mind_key val lookup_mind : mutual_inductive -> env -> mutual_inductive_body - |