coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-06-08	Test goal range in "only" selectors	Gaëtan Gilbert
	I don't know what goal_selector.v was supposed to test but CI says nobody relied on it.
2018-04-29	Strict focusing using Default Goal Selector.	Gaëtan Gilbert
	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.
2016-06-30	Goal selectors now use the keyword [only].	Cyprien Mangin
	This fixes some parsing problems when doing things like [let n := 2 in idtac n]. See bug #4877.
2016-06-14	Ident selectors cannot be used inside an Ltac expression.	Cyprien Mangin
	They can still be used at the toplevel.
2016-06-14	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin
	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.
2016-06-14	Remove the need for brackets in goal selectors.	Cyprien Mangin

2016-06-14	Add test-suite file for goal selectors.	Cyprien Mangin