coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
*	Delay use of flag "Discriminate Introduction" from interp to execution time.	Hugo Herbelin	2017-10-26
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Fix BZ#5697: Congruence does not work with primitive projections.	Pierre-Marie Pédrot	2017-08-29
*	better `try with` scope in `discr_positions`	amblaf	2017-07-31
*	Correcting [build_discriminator] to make the test-suite pass	amblaf	2017-07-31
*	Remove references to Global.env in tactics/*.ml	amblaf	2017-07-31
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Deprecate options that were introduced for compatibility with 8.4.	Guillaume Melquiond	2017-06-14
*	Deprecate options that were introduced for compatibility with 8.2.	Guillaume Melquiond	2017-06-14
*	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
*	Remove support for Coq 8.3.	Guillaume Melquiond	2017-06-14
*	Remove support for Coq 8.2.	Guillaume Melquiond	2017-06-14
*	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
*	tactics cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
*	Equality cleanup: remove constr_of_global	Matthieu Sozeau	2017-05-29
*	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\
\| *	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Stopping injection not to work on discriminable atoms (see #4890).	Hugo Herbelin	2017-05-17
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[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 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
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Chasing a few unsafe constr coercions.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Evar-normalizing functions now act on EConstrs.	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
* \|	Removing compatibility layers in Retyping	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
* \|	Equality API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Hipattern 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
* \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14