diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-06 17:21:44 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:25:30 +0100 |
commit | e27949240f5b1ee212e7d0fe3326a21a13c4abb0 (patch) | |
tree | bf076ea31e6ca36cc80e0f978bc63d112e183725 /pretyping/typing.mli | |
parent | b365304d32db443194b7eaadda63c784814f53f1 (diff) |
Typing API using EConstr.
Diffstat (limited to 'pretyping/typing.mli')
-rw-r--r-- | pretyping/typing.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 04e5e40bc..3c1c4324d 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -14,33 +14,33 @@ open Evd and universes. *) (** Typecheck a term and return its type. May trigger an evarmap leak. *) -val unsafe_type_of : env -> evar_map -> constr -> types +val unsafe_type_of : env -> evar_map -> EConstr.constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types +val type_of : ?refresh:bool -> env -> evar_map -> EConstr.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 +val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.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 -> EConstr.types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val e_check : env -> evar_map ref -> constr -> types -> unit +val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) -val e_solve_evars : env -> evar_map ref -> constr -> constr +val e_solve_evars : env -> evar_map ref -> EConstr.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 -> constr -> constr -> +val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.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 -> types array -> unsafe_judgment array -> unit + Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit |