]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
* added embedding test (HTML)
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index e7d7036632e145c43698e017b14111890dcce1f8..b09f0a8ef1bd340eb41e2d127f3b6aae8bed1964 100644 (file)
@@ -57,8 +57,7 @@ let refine metasenv context term =
     | CicRefine.Uncertain _ ->
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
-    | _ ->
-        (* TODO we should catch only the RefineFailure excecption *)
+    | CicRefine.RefineFailure _ ->
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko