coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Tactic_debug to Hightactic.	Pierre-Marie Pédrot	2016-03-20
*	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
*	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20
*	Moving Refine to its proper module.	Pierre-Marie Pédrot	2016-03-20
*	Merge branch 'v8.5'	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
* \|	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
* \|	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
\| \| *	Fix bug #4627: records with no declared arity can be template polymorphic.	Matthieu Sozeau	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