coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
*	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
*	ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file	Matej Kosik	2015-12-18
*	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
*	Adding a token "index" representing positions (1st, 2nd, etc.).	Hugo Herbelin	2015-12-15
*	Tactics: Generalizing the use of the experimental clearing modifier to	Hugo Herbelin	2015-12-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Fixing the "parsing rules with idents later declared as keywords" problem.	Hugo Herbelin	2015-11-26
* \|	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-30
\|\\|
\| *	Manually expand red_tactic so that notations do not break reduction tactics. ...	Guillaume Melquiond	2015-10-30
\| *	Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)	Guillaume Melquiond	2015-10-29
* \|	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
* \|	Removing unused code in Pcoq.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe Egramml.grammar_prod_item.	Pierre-Marie Pédrot	2015-10-27
* \|	Finer type for Pcoq.interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	Getting rid of most uses of unsafe_grammar_extend.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe Egramml.make_rule.	Pierre-Marie Pédrot	2015-10-27
* \|	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
* \|	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26
* \|	Getting rid of the Atactic entry.	Pierre-Marie Pédrot	2015-10-25
* \|	Getting rid of the Agram entry.	Pierre-Marie Pédrot	2015-10-25
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
* \|	Turn Pcoq into a regular ML file.	Pierre-Marie Pédrot	2015-10-21
* \|	Expanding the grammar extensions of Pcoq.	Pierre-Marie Pédrot	2015-10-21
* \|	Removing the dependencies of Pcoq in IFDEF macros.	Pierre-Marie Pédrot	2015-10-21
* \|	Expliciting some uses of Compat module.	Pierre-Marie Pédrot	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Allowing empty bound universe variables.	Pierre-Marie Pédrot	2015-10-08
\| *	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	Record fields accept an optional final semicolon separator.	Pierre-Marie Pédrot	2015-10-07
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	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
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\\|
\| *	Hacking parser so as to support both [> ... ] and [id].	Hugo Herbelin	2015-09-08