coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| * \|	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
\| *	Fix #4591: Uncaught exception in directory browsing.	Pierre-Marie Pédrot	2016-03-15
\| *	CoqIDE is more resilient to initialization errors.	Pierre-Marie Pédrot	2016-03-15
\| *	Tentative fix for bug #4614: "Fully check the document" is uninterruptable.	Pierre-Marie Pédrot	2016-03-15
\| *	Try eta-expansion of records only on non-recursive ones	Matthieu Sozeau	2016-03-15
\| *	Fix bug when a sort is ascribed to a Record	Matthieu Sozeau	2016-03-15
\| *	Trying to circumvent hdiutil error 5341 by padding.	Maxime Dénès	2016-03-14
* \|	Fix the comment of Refine.refine	Matthieu Sozeau	2016-03-14
* \|	Typeclasses: respect Declare Instance priority	Matthieu Sozeau	2016-03-14
* \|	Try eta-expansion of records only on non-recursive ones	Matthieu Sozeau	2016-03-14
* \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \|	Adding a few functions on type union.	Hugo Herbelin	2016-03-13
* \|	Adding a file summarizing the inconsistencies in interpreting implicit	Hugo Herbelin	2016-03-13
* \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \|	A more explicit name to the asymmetric boolean flag.	Hugo Herbelin	2016-03-12
* \|	Removing an empty file detected by Luc Grateau.	Hugo Herbelin	2016-03-12
\| *	According to Bruno, my fix for #4588 seems to be enough.	Maxime Dénès	2016-03-11
\| *	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
\| *	Hashconsing modules.	Pierre-Marie Pédrot	2016-03-10
* \|	Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi...	Hugo Herbelin	2016-03-09
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fix test-suite file coq-prog-args	Matthieu Sozeau	2016-03-09
* \| \|	Redo fix init_setoid -> init_relation_classes	Matthieu Sozeau	2016-03-09
\| * \|	Fixed bug #4533 with previous Keyed Unification commit	Matthieu Sozeau	2016-03-09
\| * \|	Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)	Enrico Tassi	2016-03-09
\| * \|	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
\| * \|	Adding backtraces to scheme error messages.	Pierre-Marie Pédrot	2016-03-07