diff options
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 04e5e40b..0ff724a1 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,13 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Names +open Constr open Environ +open EConstr open Evd (** This module provides the typing machine with existential variables @@ -24,7 +28,7 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) -val e_sort_of : env -> evar_map ref -> types -> sorts +val e_sort_of : env -> evar_map ref -> types -> Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val e_check : env -> evar_map ref -> constr -> types -> unit @@ -42,5 +46,12 @@ 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.t -> env -> evar_map ref -> +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> Names.Name.t array -> types array -> unsafe_judgment array -> unit + +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment +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 |