coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
*	Merge PR #7863: Remove Sorts.contents	Pierre-Marie Pédrot	2018-06-27
\|\
* \	Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft	Hugo Herbelin	2018-06-26
\|\ \
* \ \	Merge PR #7906: universes_of_constr don't include universes of monomorphic co...	Pierre-Marie Pédrot	2018-06-26
\|\ \ \
\| \| \| *	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
\| \|_\|/ \|/\| \|
\| * \|	universes_of_constr don't include universes of monomorphic constants	Gaëtan Gilbert	2018-06-26
* \| \|	Merge PR #7827: [engine] safe [add_unification_pb] interface	Pierre-Marie Pédrot	2018-06-23
\|\ \ \ \| \|/ / \|/\| \|
* \| \|	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\ \ \
* \| \| \|	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
\| * \| \|	Remove reference name type.	Maxime Dénès	2018-06-18
\|/ / /
\| \| *	evd: restrict_evar with candidates, can raise NoCandidatesLeft	Matthieu Sozeau	2018-06-15
\| \|/ \|/\|
\| *	evd/evarutil: safe [add_unification_pb] interface, taking EConstr's	Matthieu Sozeau	2018-06-15
\|/
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	Add a bit of doc to EConstr.decompose_lam*	Gaëtan Gilbert	2018-06-08
*	Merge PR #7706: Fix wrong deprecation msg	Pierre-Marie Pédrot	2018-06-07
\|\
* \	Merge PR #6874: [econstr] Some minor tweaks	Pierre-Marie Pédrot	2018-06-07
\|\ \
\| \| *	Update evarutil.mli	Matthieu Sozeau	2018-06-05
\| \| *	Fix wrong deprecation msg	Matthieu Sozeau	2018-06-05
\| \|/ \|/\|
* \|	Merge PR #7495: Fix restrict_universe_context	Matthieu Sozeau	2018-06-05
\|\ \
\| \| *	[econstr] Remove some Unsafe.to_constr use.	Emilio Jesus Gallego Arias	2018-06-04
\| \| *	[termops] Update type of function, anyways not used in the codebase.	Emilio Jesus Gallego Arias	2018-06-04
\| \|/ \|/\|
* \|	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \
* \| \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
* \| \|	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias	2018-05-30
* \| \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
\| \| *	Fix restrict_universe_context	Gaëtan Gilbert	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
\|/ /
* \|	Collecting Map.smart_* functions into a module Map.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
* \|	Split off Universes functions for minimization.	Gaëtan Gilbert	2018-05-17
* \|	Make Universes.refresh_constraints internal to UState	Gaëtan Gilbert	2018-05-17
* \|	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
* \|	Move solve_constraint_system near its only use site (comInductive)	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
* \|	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
\|\ \
\| * \|	Use evd_combX in Cases.	Gaëtan Gilbert	2018-05-14
\| * \|	Convert clear_hyps_in_evi to state passing style.	Gaëtan Gilbert	2018-05-11
\| * \|	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
* \| \|	Don't use ref universe_opt_subst	Gaëtan Gilbert	2018-05-08
\|/ /
* \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
* \|	Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_subst	Pierre-Marie Pédrot	2018-05-03
\|\ \
* \ \	Merge PR #6935: Separate universe minimization and evar normalization functions	Pierre-Marie Pédrot	2018-04-30
\|\ \ \
\| \| * \|	Implement to_constr with nf_evars_and_universes_opt_subst	Gaëtan Gilbert	2018-04-29
\| \| * \|	Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evars	Gaëtan Gilbert	2018-04-28
\| \|/ / \|/\| \|