From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Feb 2004 10:58:17 +0000 (+0000)
Subject: Added a TODO (to catch only the right exceptions instead of everything).
X-Git-Tag: V_0_2_3~55
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be4ee4049f0da7dd4131c3f2c56c7d1f46c87ba7;p=helm.git

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 657eb5485..f753b30ae 100644
--- 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