diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index f7ea9352b7..1c07a7ed34 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -36,10 +36,11 @@ val inh_coerce_to_sort : val inh_conv_coerce_to : Rawterm.loc -> env -> 'a evar_defs -> unsafe_judgment -> constr -> unsafe_judgment +(*i (* [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 -> (Rawterm.loc * unsafe_judgment) list -> (Rawterm.loc * unsafe_judgment) -> constr option -> unsafe_judgment - +i*) |