coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
\| \|/ / \|/\| \|
* \| \|	Merge PR #6892: Cleanup implementation of normalize_context_set a bit	Pierre-Marie Pédrot	2018-04-28
\|\ \ \
* \ \ \	Merge PR #6866: Slight improvement of messages related to direct and indirect...	Pierre-Marie Pédrot	2018-04-25
\|\ \ \ \
* \ \ \ \	Merge PR #307: Adding a flag to support different naming modes for evar hypot...	Pierre-Marie Pédrot	2018-04-24
\|\ \ \ \ \
\| \| * \| \| \|	Improving error message for clear tactic (and indirect uses of it).	Hugo Herbelin	2018-04-24
\| * \| \| \| \|	Adding a flag to support different naming modes for evar hypotheses.	Hugo Herbelin	2018-04-24
\| \|/ / / /
* / / / /	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias	2018-04-23
\|/ / / /
\| \| * /	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert	2018-04-17
\| \|/ / \|/\| \|
\| * \|	univ minimization: comment [enforce_uppers]	Gaëtan Gilbert	2018-04-13
\| * \|	univ minimization [enforce_upper]: replace Option.get with match	Gaëtan Gilbert	2018-04-13
\| * \|	univ minimization: Partially let-lift [enforce_uppers]	Gaëtan Gilbert	2018-04-13
\| * \|	univ minimization: rename acc' -> enforce_uppers	Gaëtan Gilbert	2018-04-13
\| * \|	univ minimization: use shadowing more	Gaëtan Gilbert	2018-04-13
\| * \|	univ minimization: let-lift [not_lower]	Gaëtan Gilbert	2018-04-13