summaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /pretyping/evarconv.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml20
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