coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\
\| *	Fixing output test Notations2.	Hugo Herbelin	2016-04-22
\| *	Mention problems with fix of #4582 in CHANGES.	Maxime Dénès	2016-04-22
\| *	Mention #4548 (fixed) in CHANGES.	Maxime Dénès	2016-04-22
* \|	Adding an OCaml printer for pre-initialization anomalies.	Pierre-Marie Pédrot	2016-04-20
* \|	Do that "make" in test-suite writes failures as a default together	Hugo Herbelin	2016-04-19
\| *	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
\| *	Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug.	Hugo Herbelin	2016-04-19
\| *	Revert "Fixing printing of surrounding parentheses in "ltac:"."	Hugo Herbelin	2016-04-19
* \|	Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)	Frédéric Besson	2016-04-18
\| *	Building lazily a few debugging messages involving expressions of commands	Hugo Herbelin	2016-04-17
\| *	Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode.	Hugo Herbelin	2016-04-17
\| *	Fixing printing of surrounding parentheses in "ltac:".	Hugo Herbelin	2016-04-17
* \|	Updating OCaml version number needed for 8.6.	Hugo Herbelin	2016-04-17
\| *	Add changelog for 8.5pl1 after the fact.	Maxime Dénès	2016-04-17
\| *	Build stm debugging messages lazily so that they are not silently	Hugo Herbelin	2016-04-15
* \|	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
\|/ /
\| *	A fix to #4666 (Exc_located capsule added by camlp5 overwriting	Hugo Herbelin	2016-04-12
\| *	Quick fix for #4603 (part 2): Anomaly: Universe undefined	Maxime Dénès	2016-04-12
\| *	FIX: HTML version of Chapter 4 of the Reference Manual	Matej Kosik	2016-04-12
* \|	Fixing printing of "destruct in" after ce71ac17268f.	Hugo Herbelin	2016-04-12
\| *	TYPOGRAPHY: adding missing \noindent macros	Matej Kosik	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
\|\ \
\| \| *	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