X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fnumber_notation.ml;h=d23817f0d81fa8c0794de0e9351ddc8e2f5fafd7;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=c41a9aab091034a8f81610b914721fc66b0c1ff3;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index c41a9aab0..d23817f0d 100644
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -49,7 +49,7 @@ let interp_natural_number num =
 
 let _ =
   DisambiguateChoices.add_num_choice
-    ("natural number", `Num_interp interp_natural_number);
+    ("natural number", `Num_interp interp_natural_number); (*
   DisambiguateChoices.add_num_choice
     ("Coq natural number",
       `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
@@ -76,3 +76,4 @@ let _ =
             HelmLibraryObjects.build_bin_pos num ]
         else
           assert false))
+          *)