diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 03:17:25 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | 767ecfec49543b70a605d20b1dae8252e1faabfe (patch) | |
| tree | 2b91f76b9f6c5148c7ba5e2b7cab14218d569259 /vernac/egramml.ml | |
| parent | 13929f39f8560cfcb3aacf20c84c6dcb5295cec5 (diff) | |
[parsing] Make grammar rules private.
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
Diffstat (limited to 'vernac/egramml.ml')
| -rw-r--r-- | vernac/egramml.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/egramml.ml b/vernac/egramml.ml index bcd8de1ff4..175217803f 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -45,8 +45,8 @@ let rec ty_rule_of_gram = function AnyTyRule r let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function -| TyStop -> Pcoq.Stop -| TyNext (rem, tok, _) -> Pcoq.Next (ty_erase rem, tok) +| TyStop -> Pcoq.G.Rule.stop +| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r @@ -62,7 +62,7 @@ let make_rule f prod = let symb = ty_erase ty_rule in let f loc l = f loc (List.rev l) in let act = ty_eval ty_rule f in - Pcoq.Rule (symb, act) + Pcoq.G.Production.make symb act let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function | TUentry a -> ExtraArg a |