diff options
| author | Cyprien Mangin | 2016-06-03 10:24:36 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:31 +0200 |
| commit | 98ed04803e022e66e17f91526ef708484fd17217 (patch) | |
| tree | bc123047c60c6a9fee3a90d832824d6df62bffee /ltac | |
| parent | 9356f42d5f84f9b325f71bab041d1b8184384a21 (diff) | |
Goal selectors are now tacticals and can be used as such.
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 11 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 1 |
3 files changed, 9 insertions, 5 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 3b9c58ceb1..5f52b67119 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -119,7 +119,8 @@ GEXTEND Gram (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (tc,Some s) ] + TacAbstract (tc,Some s) + | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ] (*End of To do*) | "2" RIGHTA [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) @@ -305,15 +306,15 @@ GEXTEND Gram range_selector_or_nth: [ [ n = natural ; "-" ; m = natural; l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - Vernacexpr.SelectList ((n, m) :: Option.default [] l) + SelectList ((n, m) :: Option.default [] l) | n = natural; l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - Option.cata (fun l -> Vernacexpr.SelectList ((n, n) :: l)) (Vernacexpr.SelectNth n) l ] ] + Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] ; selector: [ [ l = range_selector_or_nth; ":" -> l - | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id - | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ] + | "?" ; test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id + | IDENT "all" ; ":" -> SelectAll ] ] ; tactic_mode: [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ] diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 7cda7d1377..a72fb0d061 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -624,6 +624,8 @@ and intern_tactic_seq onlytac ist = function | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l) | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac) | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a + | TacSelect (sel, tac) -> + ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac) (* For extensions *) | TacAlias (loc,s,l) -> diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index ab61c8abba..56812b5546 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1252,6 +1252,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with strbrk "There is an \"Info\" command to replace it." ++fnl () ++ strbrk "Some specific verbose tactics may also exist, such as info_eauto."); eval_tactic ist tac + | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias (loc,s,l) -> let (ids, body) = Tacenv.interp_alias s in |