aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/extend.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/extend.mli')
-rw-r--r--parsing/extend.mli5
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 00ffb2097..da77f531d 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -51,8 +51,7 @@ val interp_grammar_command : string -> Coqast.t list -> grammar_command
(* Dealing with precedences *)
type precedence = int * int * int
-
-type parenRelation = L | E | Any
+type parenRelation = L | E | Any | Prec of precedence
(* Checks if the precedence of the parent printer (None means the
highest precedence), and the child's one, follow the given
@@ -72,7 +71,7 @@ type ppbox =
| PpTB
type unparsing_hunk =
- | PH of Ast.pat * (string * tolerability option) option * parenRelation
+ | PH of Ast.pat * string option * parenRelation
| RO of string
| UNP_BOX of ppbox * unparsing_hunk list
| UNP_BRK of int * int