From fa40e1051d879aac77bd576d4a71d937a8d029a9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Nov 2005 19:52:24 +0000 Subject: [PATCH] dded missing catch for coercions --- helm/ocaml/cic_unification/cicUnification.ml | 6 +++--- helm/ocaml/cic_unification/coercGraph.ml | 10 ++++++++-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index ea0353182..9a87bc51b 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -594,11 +594,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ if t1 = t2 then subst, metasenv,ugraph else - raise (UnificationFailure (lazy "6.2")) - (* (sprintf + raise (UnificationFailure (lazy + (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + (CicMetaSubst.ppterm subst t2)))) | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 2e69c6486..b3bc8d8b0 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -67,13 +67,19 @@ let look_for_coercion src tgt = * (source, list of coercions to follow, target) *) let get_closure_coercions src tgt uri coercions = + let eq_carr s t = + try + CoercDb.eq_carr s t + with + | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false + in match src,tgt with | CoercDb.Uri _, CoercDb.Uri _ -> let c_from_tgt = - List.filter (fun (f,_,_) -> CoercDb.eq_carr f tgt) coercions + List.filter (fun (f,_,_) -> eq_carr f tgt) coercions in let c_to_src = - List.filter (fun (_,t,_) -> CoercDb.eq_carr t src) coercions + List.filter (fun (_,t,_) -> eq_carr t src) coercions in (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @ (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @ -- 2.39.2