coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
*	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
*	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] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Properly handling parameters of primitive projections in cctac.	Pierre-Marie Pédrot	2017-08-29
*	Correcting [build_discriminator] to make the test-suite pass	amblaf	2017-07-31
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot	2017-06-13
*	Explicit the unsafe flag of all calls to Refine.refine.	Pierre-Marie Pédrot	2017-06-13
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Equality cleanup: remove constr_of_global	Matthieu Sozeau	2017-05-29
*	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Make congruence reuse discriminate instead of rolling its own.	Gaetan Gilbert	2017-05-03
\| *	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
\| *	Removing tactic compatibility layer in congruence.	Pierre-Marie Pédrot	2017-04-24
\| *	Fix the API of the new pf_constr_of_global.	Pierre-Marie Pédrot	2017-04-24
\|/
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	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
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
*	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
*	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
*	Cc API using EConstr.	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
*	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \|	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
\|/
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\
\| *	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04