From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 Oct 2002 14:07:17 +0000 (+0000)
Subject: New euristich for the unification: convertible terms always unify.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7b9103a2b7e97aedb6057cf5d6a4997f9123766e;p=helm.git

New euristich for the unification: convertible terms always unify.
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 612931ed4..f7c19073b 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -287,7 +287,11 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
         subst, metasenv
        else
         raise UnificationFailed
-   | (_,_) -> raise UnificationFailed
+   | (_,_) ->
+       if R.are_convertible context t1 t2 then
+        subst, metasenv
+       else
+        raise UnificationFailed
 
 and fo_unif_subst_exp_named_subst subst context metasenv
  exp_named_subst1 exp_named_subst2