coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Vm_compute: taking into account let-ins in parameters of constructors.	Hugo Herbelin	2017-12-14
* \| \| \| \| \| \| \|	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \|/\|
\| \| \| \| * \| \| \|	Decompiling pattern-matching: mini-removal dead code.	Hugo Herbelin	2017-12-12
\| \| \| \| * \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| \| \| \| * \| \| \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
\| \| \| * \| \| \| \|	Further clean-up in Reductionops, removing unused lift arguments.	Maxime Dénès	2017-12-12
\| \| \| \| \|_\|/ / \| \| \| \|/\| \| \|
* \| \| / \| \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| * \| \| \|	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6338: Remove up-to-conversion term matching	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| * \| \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / / \|/\| \| \| \|
\| \| * \| \|	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / \|/\| \| \|
\| * \| \|	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot	2017-12-09
* \| \| \|	Getting rid of the Update constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
* \| \| \|	Getting rid of the Shift constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
\|/ / /
\| * \|	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
* \| \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\|/ /
* \|	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...	Maxime Dénès	2017-11-30
\|\ \
\| \| *	Remove unused boolean from cl_context field of Typeclasses.typeclass	Gaëtan Gilbert	2017-11-30
\| \|/ \|/\|
\| *	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
\| *	Moving non-recursive function sort_family_of out of the retype block of recur...	Hugo Herbelin	2017-11-28
* \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \
* \| \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \|/ \|/\|
\| *	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25
\| *	Use Maps and ids for universe binders	Gaëtan Gilbert	2017-11-24
\|/
*	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
\| \|/ / \|/\| \|