diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 00:29:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:27 +0100 |
| commit | ca993b9e7765ac58f70740818758457c9367b0da (patch) | |
| tree | a813ef9a194638afbb09cefe1d1e2bce113a9d84 /pretyping/pretyping.mli | |
| parent | c2855a3387be134d1220f301574b743572a94239 (diff) | |
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 603b9f9ea..2f3ce3afa 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -110,11 +110,11 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> (** Idem but returns the judgment of the understood term *) val understand_judgment : env -> evar_map -> - glob_constr -> unsafe_judgment Evd.in_evar_universe_context + glob_constr -> EConstr.unsafe_judgment Evd.in_evar_universe_context (** Idem but do not fail on unresolved evars (type cl*) val understand_judgment_tcc : env -> evar_map ref -> - glob_constr -> unsafe_judgment + glob_constr -> EConstr.unsafe_judgment val type_uconstr : ?flags:inference_flags -> @@ -145,11 +145,11 @@ val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit (** Internal of Pretyping... *) val pretype : int -> bool -> type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_judgment + ltac_var_map -> glob_constr -> EConstr.unsafe_judgment val pretype_type : int -> bool -> val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_type_judgment + ltac_var_map -> glob_constr -> EConstr.unsafe_type_judgment val ise_pretype_gen : inference_flags -> env -> evar_map -> @@ -163,5 +163,5 @@ val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (types -> env -> evar_map -> unbound_ltac_var_map -> - Genarg.glob_generic_argument -> constr * evar_map) Hook.t + (EConstr.types -> env -> evar_map -> unbound_ltac_var_map -> + Genarg.glob_generic_argument -> EConstr.constr * evar_map) Hook.t |