coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #486: Make some functions on terms more robust w.r.t new term constr...	Maxime Dénès	2017-11-24
\|\
\| *	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
* \|	[api] A few more minor deprecation notices.	Emilio Jesus Gallego Arias	2017-11-22
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\|/
*	Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo...	Maxime Dénès	2017-11-20
\|\
\| *	Fix #5761: cbv on undefined evars under binders produces unbound rel	Gaëtan Gilbert	2017-11-15
* \|	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\|/
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
* \	Merge PR #6117: Fix printing anomaly in conv	Maxime Dénès	2017-11-13
\|\ \
* \ \	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\ \ \
* \ \ \	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \ \
\| \| \| * \|	Fixing missing separator in an error message.	Hugo Herbelin	2017-11-08
\| \|_\|/ / \|/\| \| \|
\| \| \| *	[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
\| \|/ \|/\|
* \|	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\ \
* \| \|	Refining PR#924 (insensitivity of projection heuristics to alphabet).	Hugo Herbelin	2017-11-05
\| * \|	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\|/ /
* \|	Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...	Maxime Dénès	2017-11-03
\|\ \
* \ \	Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph...	Maxime Dénès	2017-11-03
\|\ \ \
\| \| * \|	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin	2017-10-28
\| \|/ / \|/\| \|
* \| \|	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
* \| \|	unification: fix BZ#5692, recognize prim projs as CS projections	Matthieu Sozeau	2017-10-17
* \| \|	Properly handling projection parameters in canonical structures.	Pierre-Marie Pédrot	2017-10-17
* \| \|	Handling primitive projections in canonical structures.	Pierre-Marie Pédrot	2017-10-17
* \| \|	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\ \ \
* \ \ \	Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...	Maxime Dénès	2017-10-03
\|\ \ \ \
\| \| * \| \|	Remove some duplication between Typeops and Nativenorm.	Gaëtan Gilbert	2017-09-29
\| \| * \| \|	Remove trivial TODO comment (constants can't be template poly now).	Gaëtan Gilbert	2017-09-28
* \| \| \| \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
* \| \| \| \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\ \ \ \
* \ \ \ \	Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...	Maxime Dénès	2017-09-25
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \
\| \| \| \| * \| \|	After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.	Hugo Herbelin	2017-09-23
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| * \| \| \| \|	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin	2017-09-23
\| \| * \| \| \|	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin	2017-09-23
\| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...	Maxime Dénès	2017-09-22
\|\ \ \ \ \
\| * \| \| \| \|	Proposing meta names more distinguishable from evar names than ?M42.	Hugo Herbelin	2017-09-21
\| * \| \| \| \|	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin	2017-09-21
\| \|/ / / /
* \| \| \| \|	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias	2017-09-20
* \| \| \| \|	Merge PR #1036: Unify EConstr.t equality	Maxime Dénès	2017-09-19
\|\ \ \ \ \ \| \|/ / / / \|/\| \| \| \|
\| \| * \| \|	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès	2017-09-15
\|\ \ \ \
* \ \ \ \	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès	2017-09-15
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...	Maxime Dénès	2017-09-15
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond	2017-09-12
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| \| * \| \|	Using EConstr equality check in unification.	Pierre-Marie Pédrot	2017-09-08
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\| \|/ / / \|/\| \| \|
* \| \| \|	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04