diff options
Diffstat (limited to 'pretyping/coercion.mli')
| -rw-r--r-- | pretyping/coercion.mli | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 52cdabc06..0969387fb 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -9,20 +9,30 @@ open Environ open Evarutil (*i*) -(* Coercions. *) +(*s Coercions. *) val inh_app_fun : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment val inh_tosort_force : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment + +(* [inh_tosort env sigma j] insert a coercion into [j], if needed, in + such a way [t] reduces to a sort; it fails if no coercion is applicable *) val inh_tosort : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -val inh_ass_of_j : + +val inh_ass_of_j : env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment +(* [inh_conv_coerce_to loc env sigma j t] insert a coercion into [j], + if needed, in such a way it [t] and [j.uj_type] are convertible; it + fails if no coercion is applicable *) val inh_conv_coerce_to : Rawterm.loc -> - env -> 'a evar_defs -> unsafe_judgment -> typed_type -> unsafe_judgment + env -> 'a evar_defs -> unsafe_judgment -> constr -> unsafe_judgment -val inh_apply_rel_list : bool -> Rawterm.loc -> env -> 'a evar_defs -> +(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f + args)] of type [tycon] (if any) by inserting coercions in front of + each arg$_i$, if necessary *) +val inh_apply_rel_list : Rawterm.loc -> env -> 'a evar_defs -> unsafe_judgment list -> unsafe_judgment -> constr option -> unsafe_judgment |