diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 78c3c70b..da5c497c 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 8964 2006-06-20 13:52:21Z msozeau $ *) +(* $Id: subtac_coercion.ml 9284 2006-10-26 12:06:57Z msozeau $ *) open Util open Names @@ -91,7 +91,9 @@ module Coercion = struct let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c let rec mu env isevars t = + let isevars = ref isevars in let rec aux v = + let v = hnf env isevars v in match disc_subset v with Some (u, p) -> let f, ct = aux u in @@ -135,8 +137,9 @@ module Coercion = struct | Type x, Type y when x = y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> - let c1 = coerce_unify env a' a in + let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in + let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in let c2 = coerce_unify env' b b' in (match c1, c2 with None, None -> failwith "subtac.coerce': Should have detected equivalence earlier" |