coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	Removing the G_xml module again.	Pierre-Marie Pédrot	2015-07-22
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	Notation: use same level for "@" in constr: and pattern: (Close: #4272)	Enrico Tassi	2015-07-01
* \|	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
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Granting, undocumentedly, parsing of "Conjectures" as a synonym of	Hugo Herbelin	2015-06-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04