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 --- pretyping/typing.mli | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'pretyping/typing.mli') diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 0ff724a1..3cf43ace 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -26,18 +26,25 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Variant of [type_of] using references instead of state-passing. *) val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types +[@@ocaml.deprecated "Use [Typing.type_of]"] (** Typecheck a type and return its sort *) +val sort_of : env -> evar_map -> types -> evar_map * Sorts.t val e_sort_of : env -> evar_map ref -> types -> Sorts.t +[@@ocaml.deprecated "Use [Typing.sort_of]"] (** Typecheck a term has a given type (assuming the type is OK) *) +val check : env -> evar_map -> constr -> types -> evar_map val e_check : env -> evar_map ref -> constr -> types -> unit +[@@ocaml.deprecated "Use [Typing.check]"] (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) +val solve_evars : env -> evar_map -> constr -> evar_map * constr val e_solve_evars : env -> evar_map ref -> constr -> constr +[@@ocaml.deprecated "Use [Typing.solve_evars]"] (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) @@ -46,8 +53,8 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> (** Raise an error message if bodies have types not unifiable with the expected ones *) -val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> - Names.Name.t array -> types array -> unsafe_judgment array -> unit +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> + Names.Name.t array -> types array -> unsafe_judgment array -> evar_map val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment @@ -55,3 +62,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment -- cgit v1.2.3