coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Inlining "fun" and "forall" tokens in parser, so that alternative notations for	Hugo Herbelin	2015-04-20
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	grammar: export constr_eval	Enrico Tassi	2015-03-30
\| *	grammar: export hypident	Enrico Tassi	2015-03-30
\| *	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Qed export -> Qed exporting	Enrico Tassi	2015-03-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Fixed 3233 (fresh does not work with a qualid).	Pierre Courtieu	2015-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|