coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \|	Add a test for bug #5321: clearbody breaks typing of goal.	Pierre-Marie Pédrot	2017-04-17
* \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
* \| \| \|	Merge PR#523: [readme] Add badges for Travis and Gitter.	Maxime Dénès	2017-04-15
\|\ \ \ \
\| \| * \| \|	Fixing bug #5470 (anomaly on notations with misused "binder" type).	Hugo Herbelin	2017-04-14
\| \| * \| \|	Fixing bug #5469 (notation format not recognizing curly braces).	Hugo Herbelin	2017-04-14
\| \| * \| \|	Fix EOL characters in xml protocol documentation.	Maxime Dénès	2017-04-14
\| \| * \| \|	Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.	Maxime Dénès	2017-04-14
\| \| \|\ \ \
\| \| \| * \| \|	Fix anomaly when doing [all:Check _.] during a proof.	Gaetan Gilbert	2017-04-14
* \| \| \| \| \|	Merge PR#557: [toplevel] Don't print goals if there is no pending proof.	Maxime Dénès	2017-04-14
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#554: Update INSTALL now that -debug is the default.	Maxime Dénès	2017-04-14
\|\ \ \ \ \ \ \
\| \| \| \| * \ \ \	Merge PR#563: add XML protocol doc for 8.6	Maxime Dénès	2017-04-14
\| \| \| \| \|\ \ \ \
\| \| \| \| * \| \| \| \|	[travis] Use the lite target for fiat-crypto.	Maxime Dénès	2017-04-14
\| \| \| \| \| \|/ / / \| \| \| \| \|/\| \| \|
* \| \| \| \| \| \| \|	Merge PR#559: Fix compilation with camlp5 transitional mode.	Maxime Dénès	2017-04-14
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Fix compilation with camlp5 transitional mode.	Maxime Dénès	2017-04-14
\|/ / / / / / / /
\| \| \| \| \| * \| \|	update XML protocol doc to 8.6	Paul Steckler	2017-04-13
\| \| \| \| \| * \| \|	add XML protocol doc for 8.5	Paul Steckler	2017-04-13
\| \| \| \| \|/ / /
\| \| * \| \| \| \|	[toplevel] Don't print goals if there is no pending proof.	Emilio Jesus Gallego Arias	2017-04-13
* \| \| \| \| \| \|	Silence a few OCaml warnings.	Guillaume Melquiond	2017-04-13
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| * \| \|	Merge PR#510: Correctly identify [Time Defined.] as a defined	Maxime Dénès	2017-04-12
\| \| \| \|\ \ \
* \| \| \| \ \ \	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	[toplevel] [stm] cleanup in module open	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[stm] [nit] Centralize compile-time debug flag.	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[stm] Improve error messages on add/parse.	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[flags] Documentation and a minor tweak.	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[vernac] vernacentries.mli cleanup	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[stm] Port the toplevel to the STM.	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[stm] Move main parsing entry point to the STM.	Emilio Jesus Gallego Arias	2017-04-12
\| * \| \| \| \| \| \|	[stm] Remove edit_id.	Emilio Jesus Gallego Arias	2017-04-12
* \| \| \| \| \| \| \|	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...	Maxime Dénès	2017-04-12
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#549: Fast path in weak head reduction of applied atoms.	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	Update INSTALL now that -debug is the default.	Théo Zimmermann	2017-04-11
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#543: Sanitize instance interpretation	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#532: Clean Nsatz implementation.	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#537: Efficient side-effect abstraction	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \|	Adding a test for 'rewrite in *' when an evar is solved by side-effect.	Pierre-Marie Pédrot	2017-04-10
\| * \| \| \| \| \| \| \| \| \| \| \|	Adding a test for the correctness of normalization in legacy typeclasses.	Pierre-Marie Pédrot	2017-04-10
\| * \| \| \| \| \| \| \| \| \| \| \|	Documenting the changes introduced by the EConstr branch.	Pierre-Marie Pédrot	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Reductionops.contextual_reduction_function type"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "comment: typo"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Names.DirPath.equal"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Names.DirPath.compare"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Names.DirPath.is_empty"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "simplify: Environ.push_named"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "trivial"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "trivial"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "comments: corrected in the Context module"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	comments: corrected in the Context module	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	trivial	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	trivial	Matej Kosik	2017-04-10