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 612931ed48d12f31d40e573330760d33df63644a..f7c19073b015755c6be36edceffc8d708db4d82d 100644 (file)
--- 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