diff options
Diffstat (limited to 'checker/environ.mli')
| -rw-r--r-- | checker/environ.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/checker/environ.mli b/checker/environ.mli index d3448b12..87f143d1 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -11,7 +11,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; - env_engagement : engagement option; + env_engagement : engagement; } type env = { env_globals : globals; @@ -22,7 +22,7 @@ type env = { val empty_env : env (* Engagement *) -val engagement : env -> Cic.engagement option +val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env (* Digests *) @@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) @@ -51,7 +53,7 @@ val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool val is_projection : constant -> env -> bool -val lookup_projection : constant -> env -> projection_body +val lookup_projection : projection -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool |