coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-12	Merge PR #14046: make critical sections safe in the presence of exceptions	coqbot-app[bot]
	Reviewed-by: ejgallego Ack-by: gares Ack-by: SkySkimmer Ack-by: gadmm
2021-04-09	Make critical sections safe in the presence of exceptions	Lasse Blaauwbroek
	We introduce the `with_lock` combinator that locks a mutex in an atomic fashion. This ensures that exceptions thrown by signals will not leave the system in a deadlocked state.
2021-04-02	Remove the omega tactic and related options	Jim Fehrle

2021-02-25	Merge PR #13202: Infrastructure for fine-grained debug flags	coqbot-app[bot]
	Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego
2021-02-24	Infrastructure for fine-grained debug flags	Maxime Dénès

2021-02-16	Get rid of the compilation date from the binaries to make them more stable.	Guillaume Melquiond
	Contrarily to the comments, Coq_config.date was not the "release date" but just another "compile date".
2021-01-27	[coqtop] handle -print-module-uid after initialization	Enrico Tassi

2021-01-27	[sysinit] move initialization code from coqtop to here	Enrico Tassi
	We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits.
2021-01-27	[sysinit] new component for system initialization	Enrico Tassi
	This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
2020-12-18	Fixes #13657: vscoq needs goal uid.	Hugo Herbelin

2020-10-30	Adding support for printing goal names in CoqIDE.	Hugo Herbelin
	Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
2020-10-27	Rename misc nonterminals	Jim Fehrle

2020-10-12	Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol	coqbot-app[bot]
	Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-09	Add an XML message for "Show Proof Diffs"	Jim Fehrle
	Add menu item that uses this
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-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-02	Move CoqIDE to its own folder	Maxime Dénès
	The will make it possible to put a VsCoq toplevel in `ide/vscoq`.