diff options
| author | Pierre-Marie Pédrot | 2017-08-02 13:29:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 13:45:18 +0200 |
| commit | e50d86c836cf492a637db056b446bb4c70b2e40b (patch) | |
| tree | 6d9a7a0815f6681ad2e84c3f1ca1995fdd4c146d /src | |
| parent | ebee89f2b2d1815dbb89916363de1b1ad17890e8 (diff) | |
Properly classifying Ltac2 notations.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 20a00afa2e..f558f9b9cc 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -397,8 +397,12 @@ PRINTED BY pr_ltac2entry | [ tac2def_syn(e) ] -> [ e ] END -VERNAC COMMAND EXTEND VernacDeclareTactic2Definition CLASSIFIED AS SIDEFF -| [ "Ltac2" ltac2_entry(e) ] -> [ +let classify_ltac2 = function +| StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow +| StrVal _ | StrPrm _ | StrTyp _ -> Vernac_classifier.classify_as_sideeff + +VERNAC COMMAND EXTEND VernacDeclareTactic2Definition +| [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [ let local = Locality.LocalityFixme.consume () in Tac2entries.register_struct ?local e ] @@ -433,4 +437,3 @@ open Stdarg VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF | [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ] END - |