coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	document the Fail command	Paul Steckler	2018-01-25
*	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\
* \	Merge PR #6489: Update PNGs; mention async error handling; change query windo...	Maxime Dénès	2018-01-08
\|\ \
* \ \	Merge PR #6497: Add optimize_heap tactic for #6488	Maxime Dénès	2018-01-08
\|\ \ \
* \ \ \	Merge PR #6526: Fixing various typos in the Credits chapter.	Maxime Dénès	2018-01-08
\|\ \ \ \
\| \| \| \| *	Documentation and CHANGES for bracket with goal selector.	Théo Zimmermann	2018-01-05
\| \|_\|_\|/ \|/\| \| \|
\| \| * \|	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
\| \|/ / \|/\| \|
\| \| *	update PNGs; mention async error handling; change query window to query pane;...	Paul Steckler	2018-01-03
\| \|/ \|/\|
* \|	Fix typo in the refman.	Théo Zimmermann	2017-12-19
* \|	Merge PR #6381: A version of [time] that works on constr evaluation	Maxime Dénès	2017-12-18
\|\ \
* \ \	Merge PR #6380: Add tactics to reset and display the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \
* \ \ \	Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...	Maxime Dénès	2017-12-18
\|\ \ \ \
* \| \| \| \|	[doc] Nit on the manual.	Emilio Jesus Gallego Arias	2017-12-17
* \| \| \| \|	Merge PR #6219: Document undocumented options	Maxime Dénès	2017-12-15
\|\ \ \ \ \
\| \| \| \| * \|	Add documentation for time_constr	Jason Gross	2017-12-14
\| \| \| \|/ /
\| \| \| * /	Add doc+changelog entries for new LtacProf tactics	Jason Gross	2017-12-14
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \ \
* \ \ \ \	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\ \ \ \ \
\| \| \| * \| \|	Document Short Module Printing.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Document Rewriting Schemes (quickly).	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Document Record Elimination Schemes.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Document Asymmetric Patterns.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Document some omega options (missing Omega Oldstyle).	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Add doc for Set Debug RAKAM.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Add doc for Set Debug Cbv.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Add doc for Set Info/Debug Auto/Trivial/Eauto.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Add optindex for Set Bullet Behavior.	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Add doc for Set Congruence Verbose	Gaëtan Gilbert	2017-12-14
\| \| \| * \| \|	Fix typo in doc optindex for Typeclass Resolution ...	Gaëtan Gilbert	2017-12-14
\| \| * \| \| \|	Documenting the new options for printing "match".	Hugo Herbelin	2017-12-12
\| * \| \| \| \|	Remove deprecated appcontext and corresponding documentation.	Théo Zimmermann	2017-12-11
\| \|/ / / /
* \| \| \| \|	[make] remove unneeded generated file "tolink.ml"	Emilio Jesus Gallego Arias	2017-12-10
* \| \| \| \|	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-12-10
\|/ / / /
* \| \| \|	Merge PR #6277: Qualified import in coqchk	Maxime Dénès	2017-12-07
\|\ \ \ \
\| \| \| * \|	use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language	Paul Steckler	2017-12-05
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #890: Global universe declarations	Maxime Dénès	2017-12-05
\|\ \ \ \
* \ \ \ \	Merge PR #6300: Clarify operation of sequences, fixes #6095	Maxime Dénès	2017-12-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \
\| \| * \| \| \| \|	clarify operation of sequences, #6095	Paul Steckler	2017-12-01
\| \| \| * \| \| \|	[refman] Expand a little on global universes.	Matthieu Sozeau	2017-12-01
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| \| * \| \|	Documenting the -Q flag of coqchk.	Pierre-Marie Pédrot	2017-12-01
* \| \| \| \| \|	Merge PR #6276: Coqchk accepts filenames	Maxime Dénès	2017-12-01
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| / / / \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Documenting the possibility to pass filenames to coqchk.	Pierre-Marie Pédrot	2017-11-29
\| \| \|/ / \| \|/\| \|
\| \| * \|	use \ocaml macro in new text	Paul Steckler	2017-11-28
* \| \| \|	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\|/ / /
* \| \|	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\| * \|	use OCaml criteria for infix ops, #6212	Paul Steckler	2017-11-22
\|/ /
* \|	Rename coq-inferior.el -> inferior-coq.el to match provided feature.	Gaëtan Gilbert	2017-11-19
* \|	coq_makefile: document COQ_SRC_SUBDIRS	Enrico Tassi	2017-11-13
* \|	Documentation: "tac1 \|\| tac2" means "first [ progress tac1 \| tac2 ]",	Samuel Gruetter	2017-11-06