X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b09f0a8ef1bd340eb41e2d127f3b6aae8bed1964;hb=52f0f77f24e6a1dfd2a1b277d6ade218039ba574;hp=e7d7036632e145c43698e017b14111890dcce1f8;hpb=45b8f3d3fcc007ffd2e7891b992444908aa1a2fd;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e7d703663..b09f0a8ef 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -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