- logging of long-running actions (like update) is now sent to the

[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 192c2a9c1c96553aa139654489e6df1d90c6adc5..073e2cdf34d1dad8b99eabd82adfc2f577945102 100644 (file)
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -46,8 +46,6 @@ EXTEND
     ];
 END
 
-(* TODO a lot of hard coded URIs, move them in HelmLibraryObjects *)
-
 let _ =
     (* TODO cut-and-pasted code: here, in arit_notation.ml and
      * disambiguateChoices.ml *)
@@ -64,6 +62,7 @@ let _ =
        Cic.Appl [
          Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
            Cic.Implicit (Some `Type); t1; t2
+      ]));
   DisambiguateChoices.add_binary_op "and" "logical and"
     (mutind HelmLibraryObjects.Logic.and_URI);
   DisambiguateChoices.add_binary_op "or" "logical or"
@@ -71,3 +70,4 @@ let _ =
   DisambiguateChoices.add_unary_op "not" "logical not"
     (const HelmLibraryObjects.Logic.not_URI);
 
+(* vim:set encoding=utf8: *)