coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing ad-hoc interpretation rules for tactic notations and their genarg.	Pierre-Marie Pédrot	2015-12-21
*	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
*	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
*	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
*	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
*	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
*	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
*	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
*	Tying the loop in tactic printing API.	Pierre-Marie Pédrot	2015-12-18
*	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \|	Getting rid of the dynamic node of the tactic AST.	Pierre-Marie Pédrot	2015-12-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\ \
\| \| *	Improving over printing of let-tuple (see #4447).	Hugo Herbelin	2015-12-03
\| \|/
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: local names handling.	Matthieu Sozeau	2015-10-28
\| *	Printing of @{} instances for polymorphic references in Print and About.	Matthieu Sozeau	2015-10-28
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
\| *	Goptions: new value type: optional string	Enrico Tassi	2015-10-08
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Univs: fix printing bug #3797.	Matthieu Sozeau	2015-10-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\|
\| *	Print Assumptions shows engagement.	Maxime Dénès	2015-09-20
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| *	Revert the four previous commits and update the description of Richpp.	Pierre-Marie Pédrot	2015-08-15
\| *	More invariants in Richpp.	Pierre-Marie Pédrot	2015-08-15
\| *	More parametric type for generalized XML.	Pierre-Marie Pédrot	2015-08-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	Fixing bug #2169:	Pierre-Marie Pédrot	2015-07-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\|
\| *	Fixing printing of primitive coinductive record status.	Pierre-Marie Pédrot	2015-07-09
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
* \|	Remove other types not carried by interpretations in `Tacexpr`.	Arnaud Spiwack	2015-06-25
* \|	Remove useless `and_short_name` in interpreted level in `Tacexpr`.	Arnaud Spiwack	2015-06-25
\| *	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Add a space in cast since cast binds loosely.	Gregory Malecha	2015-06-24
* \|	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-23
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|