summaryrefslogtreecommitdiff
path: root/checker/environ.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
commita0a94c1340a63cdb824507b973393882666ba52a (patch)
tree73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /checker/environ.mli
parentcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff)
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
Diffstat (limited to 'checker/environ.mli')
-rw-r--r--checker/environ.mli18
1 files changed, 14 insertions, 4 deletions
diff --git a/checker/environ.mli b/checker/environ.mli
index a3f531dd..1541bf0d 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -1,6 +1,8 @@
open Names
open Term
+(* Environments *)
+
type globals = {
env_constants : Declarations.constant_body Cmap.t;
env_inductives : Declarations.mutual_inductive_body KNmap.t;
@@ -20,26 +22,33 @@ type env = {
env_imports : Digest.t MPmap.t;
}
val empty_env : env
+
+(* Engagement *)
val engagement : env -> Declarations.engagement option
-val universes : env -> Univ.universes
-val named_context : env -> named_context
-val rel_context : env -> rel_context
val set_engagement : Declarations.engagement -> env -> env
+(* Digests *)
val add_digest : env -> dir_path -> Digest.t -> env
val lookup_digest : env -> dir_path -> Digest.t
+(* de Bruijn variables *)
+val rel_context : env -> rel_context
val lookup_rel : int -> env -> rel_declaration
val push_rel : rel_declaration -> env -> env
val push_rel_context : rel_context -> env -> env
val push_rec_types : name array * constr array * 'a -> env -> env
+(* Named variables *)
+val named_context : env -> named_context
val push_named : named_declaration -> env -> env
val lookup_named : identifier -> env -> named_declaration
val named_type : identifier -> env -> constr
+(* Universes *)
+val universes : env -> Univ.universes
val add_constraints : Univ.constraints -> env -> env
+(* Constants *)
val lookup_constant : constant -> env -> Declarations.constant_body
val add_constant : constant -> Declarations.constant_body -> env -> env
val constant_type : env -> constant -> Declarations.constant_type
@@ -49,6 +58,7 @@ val constant_value : env -> constant -> constr
val constant_opt_value : env -> constant -> constr option
val evaluable_constant : constant -> env -> bool
+(* Inductives *)
val lookup_mind :
mutual_inductive -> env -> Declarations.mutual_inductive_body
val scrape_mind : env -> mutual_inductive -> mutual_inductive
@@ -56,6 +66,7 @@ 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 :
@@ -64,4 +75,3 @@ 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
-val lookup_alias : module_path -> env -> module_path