coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extruding the code for the Existential command from Proofview.	Pierre-Marie Pédrot	2016-03-20
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-20
\|\
* \|	Fixing the classification of Tactic Notation.	Pierre-Marie Pédrot	2016-03-20
\| *	Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving most of Ltac code to Hightactics.	Pierre-Marie Pédrot	2016-03-20
\|\ \
\| * \|	Moving Tacintern to Hightactics.	Pierre-Marie Pédrot	2016-03-20
\| * \|	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
\| * \|	Moving the tactic related code from Metasyntax to a new file.	Pierre-Marie Pédrot	2016-03-20
\| * \|	Moving Print Ltac to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
\| * \|	Moving Tactic Notation to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
\| * \|	Moving Tacinterp to Hightactics.	Pierre-Marie Pédrot	2016-03-20
\| * \|	Moving the use of Tactic_option from Obligations to G_obligations.	Pierre-Marie Pédrot	2016-03-19
\|/ /
* \|	Fixing compilation with old versions of CAMLP5.	Pierre-Marie Pédrot	2016-03-19
* \|	Fixing compilation with old versions of CAMLP5.	Pierre-Marie Pédrot	2016-03-19
* \|	Removing dead code in Genarg.	Pierre-Marie Pédrot	2016-03-19
* \|	Removing the untyped representation of genargs.	Pierre-Marie Pédrot	2016-03-19
* \|	Simplifying the EXTEND macros and making them more self-contained.	Pierre-Marie Pédrot	2016-03-19
\|\ \
\| * \|	EXTEND macros use their own internal representations.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Do not keep the argument type in ExtNonTerminal.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Further reducing the dependencies of the EXTEND macros.	Pierre-Marie Pédrot	2016-03-19
\|/ /
* \|	Removing the VernacSolve entry of the vernacular AST.	Pierre-Marie Pédrot	2016-03-19
\|\ \
\| * \|	Moving VernacSolve to an EXTEND-based definition.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Replacing the interpretation of Proof using ... with a proper code.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Moving the parsing of the Ltac proof mode to G_ltac.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Removing the dependency in VernacSolve in the STM.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Relying on Vernac classifier to flag tactics in the STM.	Pierre-Marie Pédrot	2016-03-19
\|/ /
* \|	Cleaning up and extending the expressivity of Pcoq.	Pierre-Marie Pédrot	2016-03-19
\|\ \
\| * \|	Allowing generalized rules in typed symbols.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
\| * \|	Simplifying the code of Entry.	Pierre-Marie Pédrot	2016-03-19
\|/ /
* \|	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\ \
* \ \	Rationalizing the use of the various EXTEND macros.	Pierre-Marie Pédrot	2016-03-18
\|\ \ \
\| * \| \|	Documenting the change of EXTEND macros.	Pierre-Marie Pédrot	2016-03-18
\| * \| \|	Making the EXTEND macros almost self-contained.	Pierre-Marie Pédrot	2016-03-18
\| * \| \|	ARGUMENT EXTEND made of only one entry share the same grammar.	Pierre-Marie Pédrot	2016-03-18
\| * \| \|	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
\| * \| \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
\| \| \| *	Fix bug #4627: records with no declared arity can be template polymorphic.	Matthieu Sozeau	2016-03-17
\| \| \| *	Test file for #4623.	Maxime Dénès	2016-03-17
\| \| \| *	Fix #4623: set tactic too weak with universes (regression)	Maxime Dénès	2016-03-17
\| * \| \|	Code factorization in Pcoq.	Pierre-Marie Pédrot	2016-03-17
\| * \| \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
\|/ / /
* \| \|	Removing the default value mechanism for generic arguments.	Pierre-Marie Pédrot	2016-03-17
\|\ \ \
\| * \| \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
\| * \| \|	Relying on parsing rules rather than genarg to check if an argument is empty.	Pierre-Marie Pédrot	2016-03-17
\|/ / /
* \| \|	Removing dead code in Q_util.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Reducing the number of modules linked in grammar.cma.	Pierre-Marie Pédrot	2016-03-17
\| \| *	Test file for #4624, fixed by Matthieu's bfce815bd1.	Maxime Dénès	2016-03-16