coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
*	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
*	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\ \
\| * \	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-07
\| \|\ \
\| \| * \|	Fixing what is probably a typo in Strict Proofs mode (#5062).	Hugo Herbelin	2016-09-03
* \| \| \|	CLEANUP: using \|> operator more consistently	Matej Kosik	2016-08-30
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
* \| \| \|	CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function	Matej Kosik	2016-08-24
\|/ / /
\| \| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| \| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| \| *	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\| \|/ \|/\|
* \|	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
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
* \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
* \|	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \
* \| \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
\| * \|	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/ /
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Removing the old refine tactic from the Tactics module.	Pierre-Marie Pédrot	2016-05-17
* \|	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Put the "fix" 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
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Remove extraneous space in coqtop/pg output (bug #4675).	Guillaume Melquiond	2016-05-03
* \|	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
* \|	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
* \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \|	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22