coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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 ↵	Maxime Dénès	2018-01-08
\|\ \ \| \| \| \| \| \| \| \| \|	window to query pane in text
* \ \	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 ↵	Paul Steckler	2018-01-03
\| \|/ \|/\| \| \| \| \|	pane; use color descriptions
* \|	Merge PR #6377: Removal of the FAQ LaTex document.	Maxime Dénès	2017-12-20
\|\ \
* \| \|	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 ↵	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Extraction Language command
\| \| \| \| * \|	Removing the FAQ, which has been moved to the GitHub wiki for this	Matt Quinn	2017-12-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	repository. Also removing FAQ-related build rules.
* \| \| \| \| \|	[doc] Nit on the manual.	Emilio Jesus Gallego Arias	2017-12-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`ssrnat` is mentioned, but it is not distributed with Coq.
* \| \| \| \| \|	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 ↵	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	same right-hand side.
* \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause.
\| * \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364.
* \| \| \| \| \|	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-12-10
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
* \| \| \| \|	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
\|/ / /
* \| \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \ \
* \| \| \|	Updating the current official writing of OCaml, updating Camlp4->Camlp5.	Hugo Herbelin	2017-11-25
\| \| \| \|
\| * \| \|	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\|/ / /
\| * /	use OCaml criteria for infix ops, #6212	Paul Steckler	2017-11-22
\|/ /