coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
*	Fix locality of "Hint Resolve <->" (bug #5189).	Guillaume Melquiond	2016-11-22
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\
\| *	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\| \|\
\| \| *	Fixes to compile with ocaml 4.01	Matthieu Sozeau	2016-11-07
\| * \|	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
\| \| *	Fix handling of only_classes at toplevel	Matthieu Sozeau	2016-11-03
\| \| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\| \|/
\| *	Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3	Matthieu Sozeau	2016-10-21
\| *	Fix bug #5036 autorewrite, sections and universes	Matthieu Sozeau	2016-10-20
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\ \
\| * \|	Fix bug #5036 autorewrite, sections and universes	Matthieu Sozeau	2016-09-29
\| \|/
* \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
* \|	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
* \|	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
* \|	Unplugging Pptactic from Ppvernac.	Pierre-Marie Pédrot	2016-09-08
\|/
*	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
*	Merge PR #195: Complete is_* family of term-examining tactics.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Add is_const	Jason Gross	2016-06-16
\| *	Add is_ind, is_constructor, is_proj	Jason Gross	2016-06-07
* \|	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Put the "specialize_eq" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
*	More toplevel value representation sharing.	Pierre-Marie Pédrot	2016-05-04
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Removing redundant *_TYPED AS clauses in EXTEND statements.	Pierre-Marie Pédrot	2016-04-12
*	Making Autorewrite independent from Ltac.	Pierre-Marie Pédrot	2016-03-25
*	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot	2016-03-25
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21