From 1fb0f39de8b87920d2f15f9e33929d372fa518dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 Sep 2008 15:46:08 +0000 Subject: [PATCH] fixed case of divergence --- .../cic_unification/cicUnification.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 2bcb09937..5eb75b5da 100644 --- 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); -- 2.39.2