coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \|	Extruding the print_atom primitive.	Pierre-Marie Pédrot	2016-04-10
\|/ /
* \|	Expliciting the fact that the atomic tactic type is self-contained.	Pierre-Marie Pédrot	2016-04-10
* \|	A small test of Print Ltac.	Hugo Herbelin	2016-04-09
* \|	Removing extra spaces in printing arguments of VERNAC EXTEND.	Hugo Herbelin	2016-04-09
* \|	Removing automatic printing of leading space in auto_using and	Hugo Herbelin	2016-04-09
* \|	Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...	Hugo Herbelin	2016-04-09
* \|	Simplifying code for printing VERNAC EXTEND.	Hugo Herbelin	2016-04-09
* \|	Fixing extra space in printing inductive types with no explicit type given.	Hugo Herbelin	2016-04-09
* \|	In pr_clauses, do not print a leading space by default so that it can	Hugo Herbelin	2016-04-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\ \
\| \| *	Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v	Nickolai Zeldovich	2016-04-09
\| \|/
\| *	Added compatibility coercions from Specif.v which were present in Coq 8.4.	Hugo Herbelin	2016-04-08
\| *	Fixing a source of inefficiency and an artificial dependency in the	Daniel de Rauglaudre	2016-04-08
* \|	Fixing printing of toplevel values.	Pierre-Marie Pédrot	2016-04-08
* \|	Fixing printing of Tactic Notations with tactic arguments.	Pierre-Marie Pédrot	2016-04-08
\| *	Allow to unset the refinement mode of Instance in ML	Matthieu Sozeau	2016-04-07
\| *	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-04-07
\| *	Merge PR#152: Add -compat 8.4 econstructor tactics, and tests	Maxime Dénès	2016-04-07
\| \|\
* \| \|	An example which failed in 8.5 and that d670c6b6 fixes.	Hugo Herbelin	2016-04-07
\| * \|	Use -win32 and -win64 suffixes for installer name on Windows.	Maxime Dénès	2016-04-07
\| \| *	Add -compat 8.4 econstructor tactics, and tests	Jason Gross	2016-04-05
\| \|/
\| *	Fix bug #4656	Jason Gross	2016-04-05
\| *	Update Coq84.v	Jason Gross	2016-04-04
\| *	Add compatibility Nonrecursive Elimination Schemes	Jason Gross	2016-04-04
* \|	Fix after merge, the revert of Bind Scope applies to trunk only.	Matthieu Sozeau	2016-04-04
* \|	Merge remote-tracking branch 'origin/pr/78' into trunk:	Maxime Dénès	2016-04-04
\|\ \
* \ \	Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunk	Matej Kosik	2016-04-04
\|\ \ \
* \ \ \	Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...	Matej Kosik	2016-04-04
\|\ \ \ \
\| \| * \ \	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\| \| \|\ \ \
\| \| * \| \| \|	Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...	Matthieu Sozeau	2016-04-04
\| \|/\| \| \| \| \|/\| \| \| \| \|
\| \| \| \| \| *	Fixing the "No applicable tactic" non informative error message	Hugo Herbelin	2016-04-03
* \| \| \| \| \|	Getting rid of the "_mods" parsing entry.	Pierre-Marie Pédrot	2016-04-01
* \| \| \| \| \|	Providing an API to access the parsing engine summary in a first-class way.	Pierre-Marie Pédrot	2016-03-31
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Adding a test for bug #1850.	Pierre-Marie Pédrot	2016-03-31
\| * \| \| \| \| \|	Moving the code handling tactic notations to Tacentries.	Pierre-Marie Pédrot	2016-03-31
\| * \| \| \| \| \|	Abstracting away the Summary-synchronized grammar-modifying commands.	Pierre-Marie Pédrot	2016-03-31
\| * \| \| \| \| \|	Moving the Tactic Notation entry parser from Pcoq to Tacentries.	Pierre-Marie Pédrot	2016-03-31
\|/ / / / / /
* \| \| \| \| \|	Ensuring that the type of base generic arguments contain triples.	Pierre-Marie Pédrot	2016-03-30
* \| \| \| \| \|	Removing dead code in Genarg.	Pierre-Marie Pédrot	2016-03-30
* \| \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\ \ \ \ \ \ \| \| \|_\|_\|_\|/ \| \|/\| \| \| \|
\| * \| \| \| \|	Update version number for 8.5pl1	Maxime Dénès	2016-03-29
* \| \| \| \| \|	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-03-28
* \| \| \| \| \|	Updating .gitignore.	Pierre-Marie Pédrot	2016-03-28
* \| \| \| \| \|	Fixing an evar leak in Rewrite introduced by 968dfdb15.	Pierre-Marie Pédrot	2016-03-28
* \| \| \| \| \|	Was too restrictive in syntactic definitions, not imagining that they	Hugo Herbelin	2016-03-28
\| * \| \| \| \|	Univs: fix get_current_context (bug #4603, part I)	Matthieu Sozeau	2016-03-25
* \| \| \| \| \|	Moving back some tactics not essentially related to Ltac into the tactics/ fo...	Pierre-Marie Pédrot	2016-03-25
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Moving Autorewrite back to tactics/.	Pierre-Marie Pédrot	2016-03-25
\| * \| \| \| \| \|	Making Autorewrite independent from Ltac.	Pierre-Marie Pédrot	2016-03-25
\| * \| \| \| \| \|	Moving Eqdecide to tactics/.	Pierre-Marie Pédrot	2016-03-25