From be4ee4049f0da7dd4131c3f2c56c7d1f46c87ba7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 10:58:17 +0000 Subject: [PATCH] Added a TODO (to catch only the right exceptions instead of everything). --- helm/ocaml/cic_disambiguation/disambiguate.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2