coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Arguments: cleanup + detect discrepancy rename/implicit (#3753)	Enrico Tassi	2016-09-29
*	Merge branch 'bug4723' into v8.6	Matthieu Sozeau	2016-09-29
\|\
\| *	Cleanup API, making inference_hook optional	Matthieu Sozeau	2016-09-29
* \|	Argument : assert does fail if no arg is given (fix #4864)	Enrico Tassi	2016-09-29
\| *	Fix bug #4723 and FIXME in API for solve_by_tac	Matthieu Sozeau	2016-09-28
\|/
*	Make it explicit when paths are added to the ML search paths.	Guillaume Melquiond	2016-09-09
*	Support qualified identifiers in Show Match (bug #5050).	Guillaume Melquiond	2016-08-27
*	Do not export an internal function in Namegen.	Pierre-Marie Pédrot	2016-08-25
*	Arguments: give / after last ! error detection fixed	Enrico Tassi	2016-08-23
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Remove the syntax changes introduced by this branch.	Pierre-Marie Pédrot	2016-06-15
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Put the "exact_constr" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\ \
\| * \|	Call hooks when terminating a definition proof (bug #4663).	Guillaume Melquiond	2016-05-03
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\\| \|
\| * \|	Building lazily a few debugging messages involving expressions of commands	Hugo Herbelin	2016-04-17
* \| \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \ \
* \| \| \|	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 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 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 OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
* \| \| \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \| \| \|	Moving Tactic_debug to tactics/ folder.	Pierre-Marie Pédrot	2016-03-06
* \| \| \|	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \| \| \|	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
\| * \| \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ / / /
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \ \
\| * \| \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\|/ / / /
* \| \| \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \| \| \|	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
* \| \| \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\| \| \|