coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
\| \| \| \| \| \| \| \| \| \|	`Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| \| \|	In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	[proof] Move bullets to their own module.	Emilio Jesus Gallego Arias	2017-06-12
	Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file.