aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/goal_selector.v
Commit message (Collapse)AuthorAge
* Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
| | | | | | | | | | | | We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
* Goal selectors now use the keyword [only].Gravatar Cyprien Mangin2016-06-30
| | | | | This fixes some parsing problems when doing things like [let n := 2 in idtac n]. See bug #4877.
* Ident selectors cannot be used inside an Ltac expression.Gravatar Cyprien Mangin2016-06-14
| | | | They can still be used at the toplevel.
* Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | | | | | | | | | | | 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.
* Remove the need for brackets in goal selectors.Gravatar Cyprien Mangin2016-06-14
|
* Add test-suite file for goal selectors.Gravatar Cyprien Mangin2016-06-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 06:29:36 +0000