coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	Adding tacticals tclBINDFIRST/tclBINDLAST.	Hugo Herbelin	2018-03-27
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\
* \|	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
* \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| *	Fixing a subtle bug in tclWITHHOLES.	Hugo Herbelin	2017-05-28
* \|	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
* \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| * \|	Fix the API of the new pf_constr_of_global.	Pierre-Marie Pédrot	2017-04-24
\| * \|	Removing the tclWEAK_PROGRESS tactical.	Pierre-Marie Pédrot	2017-04-24
\| * \|	Removing the tclNOTSAMEGOAL primitive from the API.	Pierre-Marie Pédrot	2017-04-24
\|/ /
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\ \
* \| \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Removing compatibility layers from Tacticals	Pierre-Marie Pédrot	2017-02-14
* \| \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Elim API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Tacticals API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| * \|	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\|/ /
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\|
\| *	Fix bug #5139: Anomalies should not be caught by \|\| / try.	Pierre-Marie Pédrot	2016-10-14
* \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
* \|	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
* \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \| \|	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
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Optimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
*	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14