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/coercion.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/coercion.mli')
| -rw-r--r-- | pretyping/coercion.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 62d4fb004..bc63d092d 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -10,6 +10,7 @@ open Evd open Names open Term open Environ +open EConstr open Glob_term (** {6 Coercions. } *) @@ -36,7 +37,7 @@ val inh_coerce_to_base : Loc.t -> (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) val inh_coerce_to_prod : Loc.t -> - env -> evar_map -> EConstr.types -> evar_map * EConstr.types + env -> evar_map -> types -> evar_map * types (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such @@ -44,16 +45,16 @@ val inh_coerce_to_prod : Loc.t -> applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) val inh_conv_coerce_to : bool -> Loc.t -> - env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment val inh_conv_coerce_rigid_to : bool -> Loc.t -> - env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) val inh_conv_coerces_to : Loc.t -> - env -> evar_map -> EConstr.types -> EConstr.types -> evar_map + env -> evar_map -> types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; |