diff options
| author | Jim Fehrle | 2018-12-21 14:14:05 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-01-23 10:37:31 -0800 |
| commit | ab7639ed91da9726f5248d9939db70df9ea18282 (patch) | |
| tree | 640a95dcc3d1bd8467e4b5ea5bb133538ce556aa /plugins | |
| parent | 0c3d8cab0c970778ed502a33c6d3ad5b444c2e68 (diff) | |
Move and rewrite documentation for intro patterns that was under
the intros tactic to its own subsection. Add grammar and examples.
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)) } |