From 623cbb7a784ce2d983608ee4a44bf386dfe01bbc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Mar 2008 17:37:02 +0000 Subject: [PATCH] Number notation for Coq is back again, waiting for the ultimate solution. Idea: raise the right exception when the Uri is not found. --- helm/software/components/cic_disambiguation/number_notation.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml index e3cc4fa0b..9dece04ec 100644 --- a/helm/software/components/cic_disambiguation/number_notation.ml +++ b/helm/software/components/cic_disambiguation/number_notation.ml @@ -29,7 +29,7 @@ let _ = DisambiguateChoices.add_num_choice ("natural number", (fun _ num _ -> LibraryObjects.build_nat (int_of_string num))); -(* DisambiguateChoices.add_num_choice + DisambiguateChoices.add_num_choice ("Coq natural number", (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); DisambiguateChoices.add_num_choice @@ -55,4 +55,3 @@ let _ = HelmLibraryObjects.build_bin_pos num ] else assert false)) -*) -- 2.39.2