coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
*	Merge branch 'v8.5'	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
* \|	Adding a universe argument to Pcoq.create_generic_entry.	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
\| *	Fix bug when a sort is ascribed to a Record	Matthieu Sozeau	2016-03-15
* \|	Typeclasses: respect Declare Instance priority	Matthieu Sozeau	2016-03-14
* \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\\|
\| *	Adding backtraces to scheme error messages.	Pierre-Marie Pédrot	2016-03-07
* \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \|	Removing dependency of Himsg in tactic files.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Tactic_debug to tactics/ folder.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot	2016-03-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\\|
\| *	Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.	Pierre-Marie Pédrot	2016-02-19
* \|	Renaming variants of Entries.local_entry	Matej Kosik	2016-02-16
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
\| *	Improving error message with missing patterns in the presence of	Hugo Herbelin	2016-02-08
* \|	Infering atomic ML entries from their grammar.	Pierre-Marie Pédrot	2016-02-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fixing bug #3826: "Incompatible module types" is uninformative.	Pierre-Marie Pédrot	2016-01-24
\| *	Fixing bug #4495: Failed assertion in metasyntax.ml.	Pierre-Marie Pédrot	2016-01-24
\| *	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
\| *	Restore warnings produced by the interpretation of the command line	Hugo Herbelin	2016-01-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Removing dynamic entries from Pcoq.	Pierre-Marie Pédrot	2016-01-17
* \|	Tactic notation printing accesses all the token data.	Pierre-Marie Pédrot	2016-01-16
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove deprecated command-line options such as "-as".	Guillaume Melquiond	2016-01-06
* \| \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \| \|	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
* \| \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02