coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...	Matthieu Sozeau	2018-06-14
\|\
* \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
* \|	Unify pre_env and env	Maxime Dénès	2018-05-28
* \|	Typing implementation doesn't use evdref.	Gaëtan Gilbert	2018-05-14
* \|	Typing: define functional alternatives to e_* functions	Gaëtan Gilbert	2018-05-14
* \|	set_solve_evars doesn't use an evar_map ref	Gaëtan Gilbert	2018-05-11
* \|	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
* \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
* \|	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\| *	Fixing #5500 (missing test in return clause of match leading to anomaly).	Hugo Herbelin	2018-03-27
\|/
*	Adding a missing unification in typing.ml.	Hugo Herbelin	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin	2018-02-20
*	Define EConstr version of [push_rec_types].	Cyprien Mangin	2018-01-19
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| *	Update various comments to use "template polymorphism"	Gaetan Gilbert	2017-04-11
\|/
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
*	Namegen primitives now apply on evar constrs.	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 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
*	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
*	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Cleaning up opening of the EConstr module in pretyping folder.	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
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evardefine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|/\|
\| *	Fixing #5077 (failure on typing a fixpoint with evars in its type).	Hugo Herbelin	2016-09-10
* \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
* \|	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
* \| \|	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20