coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	Use evd_combX in Cases.	Gaëtan Gilbert	2018-05-14
\| \| * \| \| \| \| \|	Typing implementation doesn't use evdref.	Gaëtan Gilbert	2018-05-14
\| \| * \| \| \| \| \|	Deprecate Typing.e_* functions	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
\| \| * \| \| \| \| \|	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
* \| \| \| \| \|	Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.	Pierre-Marie Pédrot	2018-05-04
\|\ \ \ \ \ \