summaryrefslogtreecommitdiff
path: root/kernel/typeops.mli
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /kernel/typeops.mli
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'kernel/typeops.mli')
-rw-r--r--kernel/typeops.mli7
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 85b2cfff..57acdfe4 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -28,7 +28,7 @@ val infer_v : env -> constr array -> unsafe_judgment array
val infer_type : env -> types -> unsafe_type_judgment
val infer_local_decls :
- env -> (Id.t * local_entry) list -> (env * Context.Rel.t)
+ env -> (Id.t * local_entry) list -> (env * Constr.rel_context)
(** {6 Basic operations of the typing machine. } *)
@@ -43,7 +43,6 @@ val type1 : types
val type_of_sort : Sorts.t -> types
val judge_of_prop : unsafe_judgment
val judge_of_set : unsafe_judgment
-val judge_of_prop_contents : Sorts.contents -> unsafe_judgment
val judge_of_type : Universe.t -> unsafe_judgment
(** {6 Type of a bound variable. } *)
@@ -100,9 +99,7 @@ val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
-val type_of_projection_constant : env -> Projection.t puniverses -> types
-
val type_of_constant_in : env -> pconstant -> types
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit
+val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit