diff options
| author | Hugo Herbelin | 2018-10-09 20:11:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:52:55 +0200 |
| commit | 988aab80e03e593c76869b113c5bcc043209d952 (patch) | |
| tree | 0c5caaf221c1355b1a6fd43a4169e935d84a691e /kernel | |
| parent | 3799939088b5aa616974a0d37de7e2616024f222 (diff) | |
Cleaning layout typeops.mli.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/typeops.mli | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 57acdfe4b5..515e22c99b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -54,11 +54,10 @@ val type_of_variable : env -> variable -> types val judge_of_variable : env -> variable -> unsafe_judgment (** {6 type of a constant } *) - +val type_of_constant_in : env -> pconstant -> types val judge_of_constant : env -> pconstant -> unsafe_judgment (** {6 type of an applied projection } *) - val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment (** {6 Type of application. } *) @@ -89,9 +88,7 @@ val judge_of_cast : unsafe_judgment (** {6 Inductive types. } *) - val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -99,7 +96,7 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_constant_in : env -> pconstant -> types +(** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit |