coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| *	Improving the API of constrexpr_ops.mli.	Hugo Herbelin	2017-03-23
\| \|/
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers in Retyping	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
* \|	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
*	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \|	CLEANUP: minor readability improvements	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
\|/
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	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
*	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
*	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
\|\
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	More conversion functions in the new tactic API.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\ \
\| * \|	Univs: fix bug #4375, accept universe binders on (co)-fixpoints	Matthieu Sozeau	2015-10-28
\| * \|	Do not pause globing in funind. (Fix bug #4382)	Guillaume Melquiond	2015-10-28
* \| \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
\|/ /
* \|	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
* \|	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau	2015-10-02
\| *	Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...	Arnaud Spiwack	2015-09-25
* \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\|/
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Function now supports puniveres	jforest	2015-04-14
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	handling Functional Scheme for required but not imported modules	Julien Forest	2014-12-11
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Fixing bug 3951	Julien Forest	2014-09-22
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05