diff options
| author | Cyprien Mangin | 2016-06-03 09:57:20 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:30 +0200 |
| commit | 9356f42d5f84f9b325f71bab041d1b8184384a21 (patch) | |
| tree | 15031e5d024e6925d65bcac5c8b0c3fd21b8b4be /ltac | |
| parent | 1e19f163b8c7a21d63165784828f4d733aa95171 (diff) | |
Remove the need for brackets in goal selectors.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index b9ed42e412..3b9c58ceb1 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -300,10 +300,19 @@ GEXTEND Gram [ [ n = natural ; "-" ; m = natural -> (n, m) | n = natural -> (n, n) ] ] ; + (* We unfold a range selectors list once so that we can make a special case + * for a unique SelectNth selector. *) + range_selector_or_nth: + [ [ n = natural ; "-" ; m = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> + Vernacexpr.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 ] ] + ; selector: - [ [ n=natural; ":" -> Vernacexpr.SelectNth n + [ [ l = range_selector_or_nth; ":" -> l | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id - | "[" ; l = LIST1 range_selector SEP "," ; "]" ; ":" -> Vernacexpr.SelectList l | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ] ; tactic_mode: @@ -331,7 +340,7 @@ let _ = declare_int_option { let vernac_solve n info tcom b = let status = Proof_global.with_current_proof (fun etac p -> let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll -> true | _ -> false in + let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info !print_info_trace in let (p,status) = Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p |