diff options
| author | Pierre-Marie Pédrot | 2016-03-31 23:35:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-31 23:35:38 +0200 |
| commit | 8d272227e4a4b4829678bfb6ecc84673bc47eeb7 (patch) | |
| tree | 3d20d152bda6bc687177b857a07096191af099fe /grammar | |
| parent | c0aefc5323cb4393297adcaffd2967ab93ab815e (diff) | |
| parent | bacba3d3ec0dd54d210bdf5045bc7e193c904b3c (diff) | |
Providing an API to access the parsing engine summary in a first-class way.
Instead of hardwiring a few special cases in Egramcoq, we allow the grammar
state to contain arbitrary data structures. This permits to extend the parsing
engine while retaining the synchronization with the global state, e.g. for use
in plugins.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index f9f3ee988e..adfbd8cfde 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -140,7 +140,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< do { Pptactic.declare_extra_genarg_pprule $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; - Egramcoq.create_ltac_quotation $se$ + Tacentries.create_ltac_quotation $se$ (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v)) ($lid:s$, None) } >> ] |