diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f388f900..bb07bf05 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -201,13 +201,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -(* This function requires to get the outermost arguments first. It is - a fold_right for backward compatibility. - - It tries to unify the suffix of 2 lists element by element and if - it reaches the end of a list, it returns the remaining elements in - the other list if there are some. -*) let ise_exact ise x1 x2 = match ise x1 x2 with | None, out -> out @@ -559,13 +552,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | MaybeFlexible v1, MaybeFlexible v2 -> begin match kind_of_term term1, kind_of_term term2 with - | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) -> + | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = ise_and i [(fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in + let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -673,13 +667,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty end | Rigid, Rigid when isLambda term1 && isLambda term2 -> - let (na,c1,c'1) = destLambda term1 in - let (_,c2,c'2) = destLambda term2 in + let (na1,c1,c'1) = destLambda term1 in + let (na2,c2,c'2) = destLambda term2 in assert app_empty; ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in + let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -733,12 +728,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd,UnifUnivInconsistency p) | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) - | Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty -> + | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)] + let na = Nameops.name_max n1 n2 in + evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then |