coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \| \| \| \| \| \|	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
\| \|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6377: Removal of the FAQ LaTex document.	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6470: Fix typo in the refman.	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6449: Let definitions must not contain side-effects when reaching t...	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6468: Fix order of let-in representation comment.	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6234: Make the micromega extraction check a regular output test.	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix warning about shadowing a global name.	Gaëtan Gilbert	2017-12-19
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix ltacprof_abstract (I think because of #6411 parallel merge).	Gaëtan Gilbert	2017-12-19
\| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \|	Fix typo in the refman.	Théo Zimmermann	2017-12-19
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \|	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot	2017-12-19
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6400: Circle CI	Maxime Dénès	2017-12-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Specific type for section definition entries.	Pierre-Marie Pédrot	2017-12-19
\| \| \| \| \| \|_\|_\|/ / / / / / \| \| \| \| \|/\| \| \| \| \| \| \| \|
\| \| \| * / \| \| \| \| \| \| \| \|	Fix order of let-in representation comment.	Jasper Hugunin	2017-12-19
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \|	Gitlab: don't ./configure in documentation job	Gaëtan Gilbert	2017-12-18
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6436: Fix #5368: Canonical structure unification fails.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6447: [make] More build fixes for static plugins and ocamlfind.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6284: Warning for absolute name masking (deprecated, should become ...	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6381: A version of [time] that works on constr evaluation	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6406: Make [abstract] nodes show up in the Ltac profile	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6305: Build with windows line endings	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[vernac] Cleanup of do_definition.	Emilio Jesus Gallego Arias	2017-12-18
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6217: Do dependencies in 1 command per file class.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Removing the FAQ, which has been moved to the GitHub wiki for this	Matt Quinn	2017-12-18
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6453: [doc] Nit on the manual.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
\| \|/ / / / / / / / / / / / / / / / / / / / /
\| \| \| * / / / / / / / / / / / / / / / / / /	[doc] Nit on the manual.	Emilio Jesus Gallego Arias	2017-12-17
\| \|_\|/ / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix build file	Jim	2017-12-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For bug 6249, Segmentation fault when building Coq on Windows 10.	Jim	2017-12-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Let definitions must not contain side-effects when reaching the kernel.	Pierre-Marie Pédrot	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[make] More build fixes for static plugins and ocamlfind.	Emilio Jesus Gallego Arias	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[stm] [ide protocol] Allow to include several commands on query.	Emilio Jesus Gallego Arias	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Overlay for unimath.	Gaëtan Gilbert	2017-12-15
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Do dependencies in 1 command per file class.	Gaëtan Gilbert	2017-12-15
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11.	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6219: Document undocumented options	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6429: 8.7.1 CHANGES.	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Fix #5368: Canonical structure unification fails.	Pierre-Marie Pédrot	2017-12-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Compatibility of the Coq macOS package with OS X 10.11.	Théo Zimmermann	2017-12-15
\| \|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Pass a ghost location for abstract	Jason Gross	2017-12-14
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Add documentation for time_constr	Jason Gross	2017-12-14