diff options
| author | Emilio Jesus Gallego Arias | 2017-11-21 14:15:37 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-21 14:19:23 +0100 |
| commit | d0305718b4141aa08675743d4f85238301f37ad7 (patch) | |
| tree | fadd301a9312d807f3b4f6650a9c6202103c4dc1 /src | |
| parent | f773caf67f46bdaf80d9fd13f49b53c9a21cb091 (diff) | |
[coq] Adapt to Coq's new functional EXTEND API.
See https://github.com/coq/coq/pull/6197
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 080fba7103..c738cb65bd 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -831,10 +831,11 @@ let classify_ltac2 = function | StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow | StrMut _ | StrVal _ | StrPrm _ | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff -VERNAC COMMAND EXTEND VernacDeclareTactic2Definition +VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTactic2Definition | [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [ - let local = Locality.LocalityFixme.consume () in - Tac2entries.register_struct ?local e + fun ~atts ~st -> let open Vernacinterp in + Tac2entries.register_struct ?local:atts.locality e; + st ] END |