coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \ \
* \| \| \|	[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
* \| \| \| \| \| \| \| \|	Merge PR #6969: [api] Remove functions deprecated in 8.8	Maxime Dénès	2018-05-31
\|\ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
* \| \| \| \| \| \| \| \| \|	Move interning the [hint_pattern] outside the Typeclasses hooks.	Gaëtan Gilbert	2018-05-30
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
\|/ / / / / / / /
* \| \| \| \| \| \| \|	Merge PR #7521: Fix soundness bug with VM/native and cofixpoints	Pierre-Marie Pédrot	2018-05-28
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Unify pre_env and env	Maxime Dénès	2018-05-28
* \| \| \| \| \| \| \| \|	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\|/ / / / / / / /
* \| \| \| \| \| \| \|	Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	Fix #7586: Anomaly "Uncaught exception Not_found".	Pierre-Marie Pédrot	2018-05-23
\| * \| \| \| \| \| \| \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
\| * \| \| \| \| \| \| \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
\| * \| \| \| \| \| \| \|	Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.	Hugo Herbelin	2018-05-23
\| * \| \| \| \| \| \| \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
\| \|/ / / / / / /
* \| \| \| \| \| \| \|	[api] Move `Vernacexpr` to parsing.	Emilio Jesus Gallego Arias	2018-05-23
* \| \| \| \| \| \| \|	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias	2018-05-23
\|/ / / / / / /
* \| \| \| \| \| \|	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
\| \| * \| \| \| \| \| \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
\| \| * \| \| \| \| \| \|	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\| \| * \| \| \| \| \| \|	Stop using Universes.subst(_opt)_univs_constr	Gaëtan Gilbert	2018-05-17
\| \| * \| \| \| \| \| \|	Make set minimization option internal to Universes	Gaëtan Gilbert	2018-05-17
\| \|/ / / / / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7359: Reduce usage of evar_map references	Pierre-Marie Pédrot	2018-05-17
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7213: Do not compute constr matching context if not used.	Matthieu Sozeau	2018-05-15
\|\ \ \ \ \ \ \ \ \