]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
added "tags" target to generate vim tags with otags
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index 552e3d30b21898eb7596194b6a7c3f7d4c263d8f..570ab894e434e7b9f45b5444e854c14b09fda6fe 100644 (file)
@@ -73,9 +73,6 @@ let refine metasenv context term ugraph =
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) msg);
           Ko,ugraph
-      | CicUnification.UnificationFailure s -> 
-        prerr_endline ("PASSADI QUI: " ^ s);
-          raise ( CicUnification.UnificationFailure s )
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try