X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=b7322afd4964d1a5dd3c1667a7ab66eb38cbc466;hb=f13efc1fff944ff0d3bd1414eae1739fead31856;hp=91b40fbee1fc1faa92868d8d01a774db3591b66f;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 91b40fbee..b7322afd4 100644
--- 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);