diff options
| author | Pierre-Marie Pédrot | 2016-03-31 18:42:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-31 19:32:40 +0200 |
| commit | b5de86be330f6c878b8f12173d46a4c250fac755 (patch) | |
| tree | bef5f918c3e40cdbccee9870b7a6c82aa8e5c6a2 /grammar | |
| parent | 63cef1ee8de62312df9afc2d515578df9c4cb9b1 (diff) | |
Moving the code handling tactic notations to Tacentries.
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) } >> ] |