....

[helm.git] / helm / software / components / lexicon / cicNotation.ml

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index bea67a0b4bbf9a9f54d1b28fd310466eaa83fad3..248e08bcb242c7ada134c5e5325eae86814e2062 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -32,19 +32,29 @@ type notation_id =
   | InterpretationId of TermAcicContent.interpretation_id
   | PrettyPrinterId of TermContentPres.pretty_printer_id
 
+let compare_notation_id x y = 
+  match x,y with
+  | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
+  | RuleId _, _ -> ~-1
+  | _, RuleId _ -> 1
+  | x,y -> Pervasives.compare x y
+
 let parser_ref_counter = RefCounter.create ()
 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 +66,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
           []