From 5580474eef409dc311f2db6e31974b4783450b23 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Apr 2005 12:40:12 +0000 Subject: [PATCH] UniverseInconsistency is now wrapper by CicRefine.type_of_aux' to RefineFailure --- helm/ocaml/cic_disambiguation/disambiguate.ml | 7 ------- helm/ocaml/cic_unification/cicRefine.ml | 7 +++++++ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index bb70ce279..570ab894e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -73,13 +73,6 @@ let refine metasenv context term ugraph = debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) msg); Ko,ugraph - | CicUniv.UniverseInconsistency s -> - prerr_endline ( - "INTERPRETAZIONE FALLITA PER UNIVERSE INCONSISTENCY:\n" ^ s); - (* non mi e' chiaro se debba essere wrappata dal typechecker o dal - * refiner, in ogni caso non andrebbe qui - *) - Ko, ugraph let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = try diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index c5f775253..4a6e6cadf 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -880,6 +880,13 @@ and type_of_aux' metasenv context t ugraph = (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; +let type_of_aux' metasenv context term ugraph = + try + type_of_aux' metasenv context term ugraph + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg) + + (* DEBUGGING ONLY let type_of_aux' metasenv context term = try -- 2.39.2