Added a TODO (to catch only the right exceptions instead of everything).

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 657eb5485a811eebd90a3a795ab044d260061949..f753b30ae714d724df1968653b0c4c14ba6f10ac 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -58,6 +58,7 @@ let refine metasenv context term =
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
     | _ ->
+        (* TODO we should catch only the RefineFailure excecption *)
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko