X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FcicNotation.ml;h=e10a89d5bf06152328349222ad516a82acfb3146;hb=ca41435a6021292ccba239aa173651c0be705b45;hp=d514c0273947084238fea63880031135b480f8eb;hpb=c0bc1be19b2bb2c5e3dd7f68880b26990b932118;p=helm.git

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index d514c0273..e10a89d5b 100644
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -38,13 +38,16 @@ let rule_ids_to_items = Hashtbl.create 113
 let process_notation st =
   match st with
   | Notation (loc, dir, l1, associativity, precedence, l2) ->
+      let l1 = 
+        CicNotationParser.check_l1_pattern l1 precedence associativity
+      in
       let item = (l1, precedence, associativity, l2) in
       let rule_id = ref [] in
       let _ =
         if dir <> Some `RightToLeft then
           let create_cb (l1, precedence, associativity, l2) =
             let id =
-              CicNotationParser.extend l1 ?precedence ?associativity
+              CicNotationParser.extend l1 
                 (fun env loc ->
                   CicNotationPt.AttributedTerm
                    (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
@@ -56,7 +59,7 @@ let process_notation st =
       let pp_id =
         if dir <> Some `LeftToRight then
           [ PrettyPrinterId
-              (TermContentPres.add_pretty_printer ?precedence ?associativity
+              (TermContentPres.add_pretty_printer 
                 l2 l1) ]
         else
           []
@@ -96,3 +99,7 @@ let set_active_notations ids =
   in
   TermAcicContent.set_active_interpretations interp_ids
 
+let reset () =
+  TermContentPres.reset ();
+  TermAcicContent.reset ()
+;;