handled difference associativity for the same level of the extensible grammar

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

diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli
index 105f3ffba58218d1c38d18843337e7bb409b95ad..22b4f64e8fd827a4ecaf48ffed49600f0f171117 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.mli
+++ b/helm/ocaml/cic_notation/cicNotationRew.mli
@@ -51,8 +51,8 @@ val lookup_interpretations:
       CicNotationPt.cic_appl_pattern) list
 
 val add_pretty_printer:
-  ?precedence:int ->
-  ?associativity:Gramext.g_assoc ->
+  precedence:int ->
+  associativity:Gramext.g_assoc ->
   CicNotationPt.term ->                             (* level 2 pattern *)
   CicNotationPt.term ->                             (* level 1 pattern *)
     pretty_printer_id