diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-12 22:27:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-12 22:27:49 +0000 |
| commit | bef7efb2c9c398e7f9fd7e38ece6f5a3c99461f3 (patch) | |
| tree | 539618ba7dfd91d45c462acf072ca88c7b717fb9 | |
| parent | 9d3bc8da6655f0a2d207014a38a0c7a1cf8a1788 (diff) | |
Removed what looks like a (very old) useless f.o. unification pass
made after s.o. unification succeeds.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d09e5f245..67990d219 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1021,16 +1021,10 @@ let w_unify2 env flags cv_pb ty1 ty2 evd = match kind_of_term c1, kind_of_term c2 with | Meta p1, _ -> (* Find the predicate *) - let evd' = - secondOrderAbstraction env flags ty2 (p1,oplist1) evd in - (* Resume first order unification *) - w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd' + secondOrderAbstraction env flags ty2 (p1,oplist1) evd | _, Meta p2 -> (* Find the predicate *) - let evd' = - secondOrderAbstraction env flags ty1 (p2, oplist2) evd in - (* Resume first order unification *) - w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd' + secondOrderAbstraction env flags ty1 (p2, oplist2) evd in | _ -> error "w_unify2" (* The unique unification algorithm works like this: If the pattern is |