handled difference associativity for the same level of the extensible grammar

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

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 7d09e2d6a5933c53c59035d6be3764a219205987..a5c4db085837cddd78b5e89af32a49142ef1e067 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -133,7 +133,7 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
+  | Notation of loc * CicNotationPt.term * Gramext.g_assoc * int *
       CicNotationPt.term
       (* level 1 pattern, associativity, precedence, level 2 pattern *)
   | Interpretation of loc *