diff options
| -rw-r--r-- | ltac/g_ltac.ml4 | 15 | ||||
| -rw-r--r-- | test-suite/success/goal_selector.v | 28 |
2 files changed, 30 insertions, 13 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index b9ed42e41..3b9c58ceb 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 diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index fc3c8a92d..9ba748e2a 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,21 +13,29 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true. Proof. do 2 dup. - repeat split. - [2, 4-99, 100-3]:idtac. - [2-5]:exact One. + 2, 4-99, 100-3:idtac. + 2-5:exact One. par:exact Zero. - repeat split. - [3-6]:swap 1 4. - [1-5]:swap 1 5. - [0-4]:exact One. + 3-6:swap 1 4. + 1-5:swap 1 5. + 0-4:exact One. all:exact Zero. - repeat split. - [1, 3]:exact Zero. - [1, 2, 3, 4]: exact One. + 1, 3:exact Zero. + 1, 2, 3, 4: exact One. - repeat split. all:apply transform. - [2, 4, 6]:apply transform. + 2, 4, 6:apply transform. all:apply transform. - [1-5]:apply transform. - [1-6]:exact One. + 1-5:apply transform. + 1-6:exact One. +Qed. + +Goal True -> True. +Proof. + intros y. + Fail 1-1:let x := y in idtac x. + 1:let x := y in idtac x. + exact I. Qed.
\ No newline at end of file |