diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /checker/environ.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'checker/environ.mli')
-rw-r--r-- | checker/environ.mli | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/checker/environ.mli b/checker/environ.mli index 1541bf0d..023acd0b 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -4,12 +4,11 @@ open Term (* Environments *) type globals = { - env_constants : Declarations.constant_body Cmap.t; - env_inductives : Declarations.mutual_inductive_body KNmap.t; + env_constants : Declarations.constant_body Cmap_env.t; + env_inductives : Declarations.mutual_inductive_body Mindmap_env.t; + env_inductives_eq : kernel_name KNmap.t; env_modules : Declarations.module_body MPmap.t; - env_modtypes : Declarations.module_type_body MPmap.t; - env_alias : module_path MPmap.t; -} + env_modtypes : Declarations.module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; env_engagement : Declarations.engagement option; @@ -59,19 +58,18 @@ val constant_opt_value : env -> constant -> constr option val evaluable_constant : constant -> env -> bool (* Inductives *) +val mind_equiv : env -> inductive -> inductive -> bool + val lookup_mind : mutual_inductive -> env -> Declarations.mutual_inductive_body -val scrape_mind : env -> mutual_inductive -> mutual_inductive + val add_mind : mutual_inductive -> Declarations.mutual_inductive_body -> env -> env -val mind_equiv : env -> inductive -> inductive -> bool (* Modules *) val add_modtype : module_path -> Declarations.module_type_body -> env -> env val shallow_add_module : module_path -> Declarations.module_body -> env -> env -val register_alias : module_path -> module_path -> env -> env -val scrape_alias : module_path -> env -> module_path val lookup_module : module_path -> env -> Declarations.module_body val lookup_modtype : module_path -> env -> Declarations.module_type_body |