X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fnumber_notation.ml;h=781deb90e210629c60c26cd75ca192f790c90191;hb=aa654b256f9deca4ed5bb2b13b87e1d69377f17d;hp=2b3ce2d601a351ae4bc81628afb6b58e9c049792;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index 2b3ce2d60..781deb90e 100644
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -28,6 +28,9 @@
 let _ =
   DisambiguateChoices.add_num_choice
     ("natural number",
+      (fun _ num _ -> LibraryObjects.build_nat (int_of_string num)));
+  DisambiguateChoices.add_num_choice
+    ("Coq natural number",
       (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
   DisambiguateChoices.add_num_choice
     ("real number",