]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_disambiguation/number_notation.ml
Release 0.5.9.
[helm.git] / helm / software / components / cic_disambiguation / number_notation.ml
index c41a9aab091034a8f81610b914721fc66b0c1ff3..d23817f0d81fa8c0794de0e9351ddc8e2f5fafd7 100644 (file)
@@ -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))
+          *)