coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-06-04	Proof_global: pass only 1 pstate when we don't want the proof stack	Gaëtan Gilbert
	Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says.
2019-03-27	[plugins] [derive] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias

2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2015-01-08	Avoiding introducing yet another convention in naming files.	Hugo Herbelin