coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Glob_ops.rename_glob_vars: fix typo	Gaëtan Gilbert	2018-07-03
*	Glob_ops.fix_kind_eq: fix typo	Gaëtan Gilbert	2018-07-03
*	Remove unused env argument to fresh_sort_in_family	Gaëtan Gilbert	2018-07-03
*	Merge PR #7080: Swapping Context and Constr and defining declarations on cons...	Maxime Dénès	2018-06-29
\|\
* \|	Deprecate Environ.retroknowledge function in favor of the projection	Gaëtan Gilbert	2018-06-28
* \|	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \
\| \| *	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
\| \|/ \|/\|
* \|	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
\| *	Handle mutual records in upper layers.	Pierre-Marie Pédrot	2018-06-24
\|/
*	Merge PR #7827: [engine] safe [add_unification_pb] interface	Pierre-Marie Pédrot	2018-06-23
\|\
* \|	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
* \|	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
* \|	Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.	whitequark	2018-06-21
* \|	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\ \
* \ \	Merge PR #6754: Better elaboration of pattern-matchings on primitive projections	Pierre-Marie Pédrot	2018-06-19
\|\ \ \
* \ \ \	Merge PR #7801: [vernac] Add option to force building really mutual induction...	Enrico Tassi	2018-06-19
\|\ \ \ \
* \ \ \ \	Merge PR #7714: Remove primitive-projection related data from the kernel	Maxime Dénès	2018-06-19
\|\ \ \ \ \
\| \| \| \| * \|	Remove reference name type.	Maxime Dénès	2018-06-18
\| \|_\|_\|/ / \|/\| \| \| \|
\| * \| \| \|	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
\| * \| \| \|	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
* \| \| \| \|	Fixes #7811 (uncaught Not_found in notation printer related to "match").	Hugo Herbelin	2018-06-17
\|/ / / /
\| \| * /	Better elaboration of pattern-matchings on primitive projections	Matthieu Sozeau	2018-06-15
\| \|/ / \|/\| \|
\| \| *	evd/evarutil: safe [add_unification_pb] interface, taking EConstr's	Matthieu Sozeau	2018-06-15
\| \|/ \|/\|
* \|	Fix deprecation warning introduced by PR 664 merge	Matthieu Sozeau	2018-06-14
* \|	Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...	Matthieu Sozeau	2018-06-14
\|\ \
* \ \	Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...	Matthieu Sozeau	2018-06-14
\|\ \ \
* \ \ \	Merge PR #7105: Getting rid of some false "collision between bound variable n...	Matthieu Sozeau	2018-06-14
\|\ \ \ \
\| \| \| \| *	[vernac] Add option to force building really mutual induction schemes	Matthieu Sozeau	2018-06-13
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
* \| \| \|	[api] Misctypes removal: tactic flags.	Emilio Jesus Gallego Arias	2018-06-12
* \| \| \|	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
* \| \| \|	[api] Misctypes removal: remove dummy alias.	Emilio Jesus Gallego Arias	2018-06-12
* \| \| \|	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
\| \| * \|	Fixes #7780 (missing lift in expanding alias under a binder in unification).	Hugo Herbelin	2018-06-12
\| \|/ / \|/\| \|
* \| \|	Merge PR #7679: Clean native compilation of primitive projections	Maxime Dénès	2018-06-05
\|\ \ \
* \ \ \	Merge PR #7004: Make `simple apply` obey `Opaque` directive.	Pierre-Marie Pédrot	2018-06-05
\|\ \ \ \
* \ \ \ \	Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...	Maxime Dénès	2018-06-05
\|\ \ \ \ \
\| \| \| * \| \|	More straightforward native compilation of primitive projections.	Pierre-Marie Pédrot	2018-06-05
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #7099: Stronger invariants in unification signature.	Matthieu Sozeau	2018-06-05
\|\ \ \ \ \
\| \| \| * \| \|	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	Preserving "canonical" form of return predicate in native_compute.	Hugo Herbelin	2018-06-04
\| \| * \| \|	Preserving "canonical" form of return predicate in vm_compute.	Hugo Herbelin	2018-06-04
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...	Matthieu Sozeau	2018-06-04
\|\ \ \ \
* \ \ \ \	Merge PR #7189: Fix #5539: algebraic universe produced by cases.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \
\| \| \| * \| \|	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31