diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-04 22:29:08 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-04 22:29:08 +0000 |
| commit | f08e50f55cc8348997e8d939e603da554d8f329c (patch) | |
| tree | f43ffacd140edbf8417324df79e5833b6ca50b92 /kernel/reduction.ml | |
| parent | 3a396ec045c723d4b62e43e7e846ccd63f5e5419 (diff) | |
Forgotten lifts in eta-expansion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13494 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 55a7ca884..cbcbd151e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -333,13 +333,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv = anomaly "conversion was given unreduced term (FLambda)"; let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr CONV infos - (lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) cuniv + (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> if v2 <> [] then anomaly "conversion was given unreduced term (FLambda)"; let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr CONV infos - (el_lift lft1,(hd1,eta_expand_stack v1)) (lft2,(bd2,[])) cuniv + (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv (* only one constant, defined var or defined rel *) | (FFlex fl1, _) -> |