diff options
| author | Théo Zimmermann | 2019-01-24 16:35:24 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-24 16:35:24 +0100 |
| commit | 1006fd52c03e7d8ea1d0b612df168f21c9b56455 (patch) | |
| tree | 4652f89acf9f1fcf3818da68b88755a19c7c3861 /plugins | |
| parent | 5a9aab76481e6ccaf311a02f18113af75eed3e7e (diff) | |
| parent | ab7639ed91da9726f5248d9939db70df9ea18282 (diff) | |
Merge PR #9269: Move and rewrite intro pattern section
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 46ea3819ac..7bf705ffeb 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram [ [ c = smart_global; nl = occs -> { (nl,c) } ] ] ; intropatterns: - [ [ l = LIST0 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST0 intropattern -> { l } ] ] ; ne_intropatterns: - [ [ l = LIST1 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST1 intropattern -> { l } ] ] ; or_and_intropattern: [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc } @@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; - nonsimple_intropattern: + intropattern: [ [ l = simple_intropattern -> { l } | "*" -> { CAst.make ~loc @@ IntroForthcoming true } | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ] @@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "eintros"; pl = ne_intropatterns -> { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) } + | IDENT "eintros" -> + { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) } |