diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3c37a49f..3074c4c4 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml 10883 2008-05-05 13:55:24Z herbelin $ *) +(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -43,6 +43,10 @@ module type S = sig val inh_coerce_to_base : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) + val inh_coerce_to_prod : loc -> + env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type + (* [inh_conv_coerce_to loc env evd 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 *) @@ -160,6 +164,8 @@ module Default = struct let inh_coerce_to_base loc env evd j = (evd, j) + let inh_coerce_to_prod loc env evd t = (evd, t) + let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) then |