]> matita.cs.unibo.it Git - helm.git/commitdiff
Wrong reported error message fixed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Nov 2005 15:38:19 +0000 (15:38 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Nov 2005 15:38:19 +0000 (15:38 +0000)
helm/ocaml/cic_disambiguation/disambiguate.ml

index 8f2747a7d6b6de6db5165a380f8bb84d4dbe8131..de3701e23401e8cec86445ce5ecbbb4a041a9337 100644 (file)
@@ -89,7 +89,7 @@ let refine_obj metasenv context uri obj ugraph =
      | CicRefine.RefineFailure msg ->
          debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
            (CicPp.ppobj obj) (Lazy.force msg))) ;
-         Ko (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
+         Ko (lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try