- factorized DisambiguateChoices module

[helm.git] / helm / ocaml / cic_disambiguation / arit_notation.ml

diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml
index f0f8d52bc32c7fc69f0c97ab3d43232dd9ab038a..e4c700d0a6fede6338256ae9a6b12d51ccbeeb93 100644 (file)
--- a/helm/ocaml/cic_disambiguation/arit_notation.ml
+++ b/helm/ocaml/cic_disambiguation/arit_notation.ml
@@ -57,28 +57,28 @@ EXTEND
 END
 
 let _ =
-  Disambiguate.add_num_choice
+  DisambiguateChoices.add_num_choice
     ("natural number",
       (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
-  Disambiguate.add_num_choice
+  DisambiguateChoices.add_num_choice
     ("real number",
       (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
-  Disambiguate.add_symbol_choice "plus"
+  DisambiguateChoices.add_symbol_choice "plus"
     ("natural plus",
      (fun env _ args ->
        let t1, t2 =
          match args with
          | [t1; t2] -> t1, t2
-         | _ -> raise Disambiguate.Invalid_choice
+         | _ -> raise DisambiguateChoices.Invalid_choice
        in
        Cic.Appl [ HelmLibraryObjects.Peano.plus; t1; t2 ]));
-  Disambiguate.add_symbol_choice "plus"
+  DisambiguateChoices.add_symbol_choice "plus"
     ("real plus",
      (fun env _ args ->
        let t1, t2 =
          match args with
          | [t1; t2] -> t1, t2
-         | _ -> raise Disambiguate.Invalid_choice
+         | _ -> raise DisambiguateChoices.Invalid_choice
        in
        Cic.Appl [ HelmLibraryObjects.Reals.rplus; t1; t2 ]));