coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Separate vim/emacs fold markers from ocamldoc comments	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Build docs for plugins by default, add NOPLUGINDOCS flag to disable	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Change non-documentation comment from ocamldoc style	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Fix formatting of some ocamldoc comments to reduce warnings	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Remove non-existent dependency	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Tweak comments to fix ocamldoc errors	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Tidy up ml-doc outut, give it a separate output directory	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Use computed deps to generate ml-doc and use implicit mli-doc deps	mrmr1993	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Deprecate Focus and Unfocus.	Théo Zimmermann	2018-03-05
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	[ssreflect] Export parsing witnesses in mli file.	Emilio Jesus Gallego Arias	2018-03-05
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Sanitize universe declaration in Context (stop using a ref...)	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	configure: -warn-error: now takes a bool so that you can also turn it off	Enrico Tassi	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	configure: profiles (sets of flags)	Enrico Tassi	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	configure: make Prefs a record rather than a module of refs	Enrico Tassi	2018-03-05
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \| \| \| \| \| \| \| \|/ / / / / / / / / / \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * / \| \| \| \| \| \| \| \| \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \| \| \| \| \| \|/ / / / / / / / / / /
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	ssr: add Prenex Implicits for Some_inj to use it as a view	Anton Trunov	2018-03-04
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	ssr: fix typo in doc comment	Anton Trunov	2018-03-04
\| \| \| \| \| \| \| \|/ / / / / / / / / \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	ssr: ipats: V82.tactic ~nf_evars:false everywhere	Enrico Tassi	2018-03-04
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Proofview: V82.tactic option to not normalize evars	Enrico Tassi	2018-03-04
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	ssr: rewrite Ssripats and Ssrview in the tactic monad	Enrico Tassi	2018-03-04
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	tactics: export e_reduct_in_concl	Enrico Tassi	2018-03-04
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	reductionops: remove dead code "bind_assum"	Enrico Tassi	2018-03-04
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	proofview: debug API to print a goal	Enrico Tassi	2018-03-04
\| \| \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6736: [toplevel] Move beautify to its own pass.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6882: Harden gitattributes against core.whitespace configuration.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6676: [proofview] goals come with a state	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #915: Fix rewrite in * side conditions	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Remove all uses of Focus in standard library.	Théo Zimmermann	2018-03-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix typos.	Théo Zimmermann	2018-03-04
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Removing test for bug #2850.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Adding a test file for evar handling in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[compat] Remove "Tactic Pattern Unification"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	[compat] Remove "Standard Proposition Elimination"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[compat] Remove "Intuition Iff Unfolding"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|