aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/goal_selector.v
AgeCommit message (Expand)Author
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2016-06-30Goal selectors now use the keyword [only].Cyprien Mangin
2016-06-14Ident selectors cannot be used inside an Ltac expression.Cyprien Mangin
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-14Remove the need for brackets in goal selectors.Cyprien Mangin
2016-06-14Add test-suite file for goal selectors.Cyprien Mangin