X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Flogic_notation.ml;h=2227b2741e14c6dd6fadac9a75ba4401ba8dc3d2;hb=a96ac1d9b14c89392c5672fb94944363ced625b8;hp=3c73aabd1cafedf81e87ca6a33150c17d659b8dd;hpb=c1a5a672088af4ff926e5848396c810c2539c2f5;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index 3c73aabd1..2227b2741 100644
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -26,19 +26,19 @@
 open CicTextualParser2
 
 EXTEND
-  term: LEVEL "add"
+  term: LEVEL "logic_add"
     [
       [ t1 = term; SYMBOL <:unicode<lor>> (* ∨ *); t2 = term ->
           return_term loc (CicAst.Appl [CicAst.Symbol ("or", 0); t1; t2])
       ]
     ];
-  term: LEVEL "mult"
+  term: LEVEL "logic_mult"
     [
       [ t1 = term; SYMBOL <:unicode<land>> (* ∧ *); t2 = term ->
         return_term loc (CicAst.Appl [CicAst.Symbol ("and", 0); t1; t2])
       ]
     ];
-  term: LEVEL "inv"
+  term: LEVEL "logic_inv"
     [
       [ SYMBOL <:unicode<lnot>> (* ¬ *); t = term ->
         return_term loc (CicAst.Appl [CicAst.Symbol ("not", 0); t])
@@ -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 *)
@@ -72,3 +70,4 @@ let _ =
   DisambiguateChoices.add_unary_op "not" "logical not"
     (const HelmLibraryObjects.Logic.not_URI);
 
+(* vim:set encoding=utf8: *)