From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/typeops.mli | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'kernel/typeops.mli') 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 -- cgit v1.2.3