fixed case of divergence

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 2bcb099370029d4a418bbb28ca28f1b5c7e53c5e..5eb75b5da73b3aa9db52ab99178410904854072c 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -599,7 +599,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                     CoercDb.is_a_coercion cc1 <> None && 
                     CoercDb.is_a_coercion cc2 <> None &&
                     not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY: 
+(*DEBUGGING ONLY:  
 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 let res =
         *)
@@ -659,7 +659,9 @@ let res =
                                 * coercions not only in coerced position *)
                                if c1 = cc1 then 
                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
-                               else Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+                               else if c2 = cc2 then
+                                 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+                               else raise exn
                            in
                             fo_unif_subst test_equality_only subst context
                              metasenv l1 l2 ugraph
@@ -692,7 +694,7 @@ let res =
                                 last,
                                   fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl1 ugraph
-                            | _ -> last_tl1,(subst,metasenv,ugraph) 
+                            | _ -> last_tl1,(subst,metasenv,ugraph)
                           in
                           let last_tl2',(subst,metasenv,ugraph) =
                            match last_tl2,to2 with
@@ -700,18 +702,19 @@ let res =
                                 last,
                                   fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl2 ugraph
-                            | _ -> last_tl2,(subst,metasenv,ugraph) 
+                            | _ -> last_tl2,(subst,metasenv,ugraph)
                           in
-                        (*DEBUGGING ONLY:
+                           let subst',metasenv,ugraph =
+                        (*DEBUGGING ONLY: 
 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
 *)
-                           let subst,metasenv,ugraph =
                             fo_unif_subst test_equality_only subst context
                              metasenv last_tl1' last_tl2' ugraph
                            in
-                            fo_unif_subst test_equality_only subst context
+                           if subst = subst' then raise exn else
+                            fo_unif_subst test_equality_only subst' context
                              metasenv (C.Appl l1) (C.Appl l2) ugraph)
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY: 
 in
 let subst,metasenv,ugraph = res in
 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);