diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 04:02:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | d5dcb490f4f08dc1f5ae4158a26d264e03f808cc (patch) | |
| tree | dc250ea98cc0983c858e9d76b49c5167400bfad9 /user-contrib | |
| parent | 767ecfec49543b70a605d20b1dae8252e1faabfe (diff) | |
[parsing] Remove extend AST in favor of gramlib constructors
We remove Coq's wrapper over gramlib's grammar constructors.
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 6 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.mli | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 8b3203c8dd..477672ebdb 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -861,7 +861,7 @@ let rules = [ ] in Hook.set Tac2entries.register_constr_quotations begin fun () -> - Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)]) + Pcoq.grammar_extend Pcoq.Constr.operconstr {G.pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]} end } diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 547ca0c2ed..0946c88228 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1590,7 +1590,7 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu) type seqrule = -| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule +| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule let rec make_seq_rule = function | [] -> diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index c5f081eab9..7c4971db8c 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -558,7 +558,7 @@ type 'a token = | TacNonTerm of Name.t * 'a type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule @@ -611,7 +611,7 @@ type synext = { type krule = | KRule : - (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.rule * + (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.G.Rule.t * ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule let rec get_rule (tok : scope_rule token list) : krule = match tok with @@ -643,7 +643,7 @@ let perform_notation syn st = | Some lev -> Some (string_of_int lev) in let rule = (lev, None, [rule]) in - ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st) + ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.G.pos=None; data=[rule]})], st) let ltac2_notation = Pcoq.create_grammar_command "ltac2-notation" perform_notation diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index 4938e96cae..1efac697aa 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit (** {5 Notations} *) type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule |