From: Claudio Sacerdoti Coen Date: Sat, 19 Nov 2005 15:26:57 +0000 (+0000) Subject: More information is now printed when reporting errors. X-Git-Tag: V_0_7_2_3~28 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f3103013aa11311dd07d618fd6530d878d6186e;p=helm.git More information is now printed when reporting errors. --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index fb0666d8d..8f2747a7d 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -68,13 +68,13 @@ let refine_term metasenv context uri term ugraph = CicRefine.type_of_aux' metasenv context term ugraph in (Ok (term', metasenv')),ugraph1 with - | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain s,ugraph + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko msg,ugraph + Ko (lazy ("Error trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph let refine_obj metasenv context uri obj ugraph = assert (context = []); @@ -83,13 +83,13 @@ let refine_obj metasenv context uri obj ugraph = let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in (Ok (obj', metasenv)),ugraph with - | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain s,ugraph + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko msg,ugraph + Ko (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try