From 7b9103a2b7e97aedb6057cf5d6a4997f9123766e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 Oct 2002 14:07:17 +0000
Subject: [PATCH] New euristich for the unification: convertible terms always
 unify.

---
 helm/ocaml/cic_unification/cicUnification.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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
-- 
2.39.2