From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- pretyping/coercion.mli | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'pretyping/coercion.mli') diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index f675beff..42ce27fd 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coercion.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: coercion.mli 8875 2006-05-29 19:59:11Z msozeau $ i*) (*i*) open Util @@ -33,13 +33,19 @@ module type S = sig type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + + (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type its base type (the notion depends on the coercion system) *) + val inh_coerce_to_base : loc -> + env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * 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 *) -- cgit v1.2.3