diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-25 18:34:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:41 +0100 |
| commit | 02dd160233adc784eac732d97a88356d1f0eaf9b (patch) | |
| tree | d2baacdc2a4ae06e4607bfe09b48ba2c23a78a0f /pretyping/typing.mli | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index bf26358a2..91134b499 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -9,46 +9,47 @@ open Names open Term open Environ +open EConstr open Evd (** This module provides the typing machine with existential variables and universes. *) (** Typecheck a term and return its type. May trigger an evarmap leak. *) -val unsafe_type_of : env -> evar_map -> EConstr.constr -> types +val unsafe_type_of : env -> evar_map -> constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * EConstr.types +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 -> EConstr.constr -> EConstr.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 -> EConstr.types -> sorts +val e_sort_of : env -> evar_map ref -> types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit +val e_check : env -> evar_map ref -> constr -> types -> unit (** Returns the instantiated type of a metavariable *) -val meta_type : evar_map -> metavariable -> EConstr.types +val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) -val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr +val e_solve_evars : env -> evar_map ref -> constr -> constr (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) -val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr -> +val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit (** Raise an error message if bodies have types not unifiable with the expected ones *) val check_type_fixpoint : Loc.t -> env -> evar_map ref -> - Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> unit + Names.Name.t array -> types array -> unsafe_judgment array -> unit -val judge_of_prop : EConstr.unsafe_judgment -val judge_of_set : EConstr.unsafe_judgment +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment val judge_of_abstraction : Environ.env -> Name.t -> - EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment + unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> - EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment + unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment |