diff options
| author | Hugo Herbelin | 2014-08-18 17:13:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:39 +0200 |
| commit | 72498d6d68ac12ba4db0db7d54f0ac6fdaaf0c61 (patch) | |
| tree | 79c10bf2a989cab52970046f1a87714f44926a2a /parsing | |
| parent | 924771d6fdd1349955c2d0f500ccf34c2109507b (diff) | |
Adding a new intro-pattern for "apply in" on the fly. Using syntax
"pat/term" for "apply term on current_hyp as pat".
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9cf476a5ea..ae4bf8a126 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -307,6 +307,8 @@ GEXTEND Gram simple_intropattern: [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat) | pat = equality_intropattern -> !@loc, IntroAction pat + | pat = simple_intropattern; "/"; c = constr -> + !@loc, IntroAction (IntroApplyOn (c,pat)) | pat = naming_intropattern -> !@loc, IntroNaming pat ] ] ; simple_binding: diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 54fcb12b06..5c0a48dd69 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -218,7 +218,7 @@ module Tactic : val int_or_var : int or_var Gram.entry val red_expr : raw_red_expr Gram.entry val simple_tactic : raw_tactic_expr Gram.entry - val simple_intropattern : intro_pattern_expr located Gram.entry + val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry |