- factorized DisambiguateChoices module

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

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index 011462f8158fcd2f68f56b17a8d93b6cbadfc7e0..85c5be3ea324fefc82d004eb7d7b03c62388855a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -47,13 +47,13 @@ EXTEND
 END
 
 let _ =
-  Disambiguate.add_symbol_choice "eq"
+  DisambiguateChoices.add_symbol_choice "eq"
     ("leibnitz's equality",
      (fun interp _ args ->
        let t1, t2 =
          match args with
          | [t1; t2] -> t1, t2
-         | _ -> raise Disambiguate.Invalid_choice
+         | _ -> raise DisambiguateChoices.Invalid_choice
        in
        Cic.Appl [
          Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);