handled difference associativity for the same level of the extensible grammar

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 91b40fbee1fc1faa92868d8d01a774db3591b66f..b7322afd4964d1a5dd3c1667a7ab66eb38cbc466 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -29,9 +29,6 @@ type pattern_id = int
 type interpretation_id = pattern_id
 type pretty_printer_id = pattern_id
 
-let default_prec = 50
-let default_assoc = Gramext.NonA
-
 module Ast = CicNotationPt
 
 type term_info =
@@ -446,9 +443,7 @@ let lookup_interpretations symbol =
       !(Hashtbl.find interpretations symbol)
   with Not_found -> raise Interpretation_not_found
 
-let add_pretty_printer
-  ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
-=
+let add_pretty_printer ~precedence ~associativity l2 l1 =
   let id = fresh_id () in
   let l2' = CicNotationUtil.strip_attributes l2 in
   Hashtbl.add level1_patterns21 id (precedence, associativity, l1);