coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)	Frédéric Besson	2016-04-18
*	Updating OCaml version number needed for 8.6.	Hugo Herbelin	2016-04-17
*	Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.	Hugo Herbelin	2016-04-15
*	This is an attempt to clarify terminology in choosing variable names	Hugo Herbelin	2016-04-14
*	Moving and enhancing the grammar_tactic_prod_item_expr type.	Pierre-Marie Pédrot	2016-04-14
*	Uniformizing the semantics of ARGUMENT EXTEND macros.	Pierre-Marie Pédrot	2016-04-13
\|\
\| *	Adding toplevel representation sharing for some generic arguments.	Pierre-Marie Pédrot	2016-04-12
\| *	Removing redundant *_TYPED AS clauses in EXTEND statements.	Pierre-Marie Pédrot	2016-04-12
\| *	Adding warnings for inferrable *_TYPED AS clauses.	Pierre-Marie Pédrot	2016-04-12
\| *	Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.	Pierre-Marie Pédrot	2016-04-12
\| *	Warning for redundant TYPED AS clauses.	Pierre-Marie Pédrot	2016-04-12
\| *	Allowing simple ARGUMENT EXTEND not to mention their self type.	Pierre-Marie Pédrot	2016-04-12
\| *	Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.	Pierre-Marie Pédrot	2016-04-12
\|/
*	Fixing printing of "destruct in" after ce71ac17268f.	Hugo Herbelin	2016-04-12
*	Removing the typed-level tactic_expr type.	Pierre-Marie Pédrot	2016-04-11
\|\
\| *	Removing the ad-hoc tactic_expr type.	Pierre-Marie Pédrot	2016-04-11
\| *	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
\|\
\| *	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