coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Use a more efficient substitution composition in evar hypothesis naming.	Pierre-Marie Pédrot	2018-01-04
*	Cleanup name-binding structure for fresh evar name generation.	Pierre-Marie Pédrot	2018-01-02
*	Merge PR #6222: Share computation of unifiable evars	Maxime Dénès	2017-12-22
\|\
* \|	[summary] Adapt STM to the new Summary API.	Emilio Jesus Gallego Arias	2017-12-09
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\| *	Experimenting with a fine-grained cache for undefined evars in evinfos.	Pierre-Marie Pédrot	2017-11-21
\|/
*	[api] Move structures deprecated in the API to the 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
*	Moving setting of "cleared" evar flag directly in Evd.restrict.	Hugo Herbelin	2017-09-27
*	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Adding intermediate entry point to create an evar in empty rel_context.	Hugo Herbelin	2017-06-25
\|/
*	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
*	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\
\| * \|	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
\| \| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \|/
* /	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	Moving evar-normalization functions to EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
*	Making Evd independent from Namegen.	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 some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
*	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Leminv API using EConstr.	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
*	Refine 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
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\
\| *	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\\|
\| *	Fast path in push_rel_context_to_named_context.	Pierre-Marie Pédrot	2016-09-05
\| *	Fast path in whd_evar.	Pierre-Marie Pédrot	2016-09-02
* \|	Removing calls of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-26
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-26
* \|	CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...	Matej Kosik	2016-08-25
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\|/
*	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
*	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05