handled difference associativity for the same level of the extensible grammar

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

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index b7a62476cf26b05a9c3d52d4a426aadca0604c7b..029152e36fdfe6eac95bfd41e51c9df323964c1d 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -248,14 +248,11 @@ let pp_l1_pattern = CicNotationPp.pp_term
 let pp_l2_pattern = CicNotationPp.pp_term
 
 let pp_associativity = function
-  | Some Gramext.LeftA -> "left associative "
-  | Some Gramext.RightA -> "right associative "
-  | Some Gramext.NonA -> "non associative "
-  | None -> ""
+  | Gramext.LeftA -> "left associative"
+  | Gramext.RightA -> "right associative"
+  | Gramext.NonA -> "non associative"
 
-let pp_precedence = function
-  | Some i -> sprintf "with precedence %d " i
-  | None -> ""
+let pp_precedence i = sprintf "with precedence %d" i
 
 let pp_command = function
   | Include (_,path) -> "include " ^ path
@@ -274,7 +271,7 @@ let pp_command = function
         (String.concat " " (List.map pp_argument_pattern arg_patterns))
         (pp_cic_appl_pattern cic_appl_pattern)
   | Notation (_, l1_pattern, assoc, prec, l2_pattern) ->
-      sprintf "notation \"%s\" %s%sfor %s"
+      sprintf "notation \"%s\" %s %s for %s"
         (pp_l1_pattern l1_pattern)
         (pp_associativity assoc)
         (pp_precedence prec)