coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-09-22	Setting default value for Display Parentheses off in CoqIDE.	Hugo Herbelin

2020-09-01	Unify the shelves	Maxime Dénès
	Before this patch, the proof engine had three notions of shelves: - A local shelf in `proofview` - A global shelf in `Proof.t` - A future shelf in `evar_map` This has lead to a lot of confusion and limitations or bugs, because some components have only a partial view of the shelf: the pretyper can see only the future shelf, tactics can see only the local and future shelves. In particular, this refactoring is needed for #7825. The solution we choose is to move shelf information to the evar map, as a shelf stack (for nested `unshelve` tacticals). Closes #8770. Closes #6292. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-26	Move given_up goals to evar_map	Maxime Dénès

2020-08-06	Repair coqide option "Display parentheses"	Jean-Christophe Léchenet

2020-06-29	Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()	Pierre-Marie Pédrot
	Reviewed-by: ppedrot
2020-06-26	[declare] Reify Proof.t API into the Proof module.	Emilio Jesus Gallego Arias
	This is in preparation for the next commit which will clean-up the current API flow in `Declare`.
2020-06-23	CoqIDE: fix lexing of UTF-8 in quotations like constr:()	James Lottes

2020-06-22	CoqIDE: accept to open files with invalid names	Vincent Laporte

2020-06-02	Move CoqIDE to its own folder	Maxime Dénès
	The will make it possible to put a VsCoq toplevel in `ide/vscoq`.