coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
*	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert	2018-05-14
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
*	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
*	Merge PR #7108: Legacy refiner handle eta-expanded case analysis	Pierre-Marie Pédrot	2018-04-23
\|\
* \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| *	Preparing old-style refine from logic.ml to deal with "Cases" proof	Hugo Herbelin	2018-03-29
* \|	Congruence: getting rid of a detour by the compatibility layer of proof engine.	Hugo Herbelin	2018-03-27
\|/
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Cosmetic: add an expected newline in proof_global.	Hugo Herbelin	2018-03-08
*	Add an invariant on future goals in Proof.run_tactic.	Hugo Herbelin	2018-03-08
*	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
*	Proof engine: using save_future_goal when relevant.	Hugo Herbelin	2018-03-08
*	Proof engine: consider the pair principal and future goals as an entity.	Hugo Herbelin	2018-03-08
*	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
*	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \
* \ \	Merge PR #6676: [proofview] goals come with a state	Maxime Dénès	2018-03-04
\|\ \ \
\| \| * \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| \|/ / \|/\| \|
\| \| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|/ \|/\|
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| *	proofview: goals come with a state	Enrico Tassi	2018-02-20
\|/
*	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\
* \|	[toplevel] Make toplevel state into a record.	Emilio Jesus Gallego Arias	2018-02-15
\| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\|/
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Fix #6591: anomaly when using selectors outside of a proof.	Cyprien Mangin	2018-01-22
*	Force polymorphic definitions to have no internal constraints.	Pierre-Marie Pédrot	2018-01-11
*	Merge PR #6264: [kernel] Patch allowing to disable VM reduction.	Maxime Dénès	2017-12-14
\|\
* \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
* \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
* \| \|	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \
* \ \ \	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \ \ \
\| \| * \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \| * \|	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|/ /
* \| / /	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot	2017-12-09
\| \|/ / \|/\| \|
\| * \|	Fix #6323: stronger restrict universe context vs abstract.	Gaëtan Gilbert	2017-12-06
\|/ /
\| *	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
* \|	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
\|/
*	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	Make restrict_universe_context stronger.	Gaëtan Gilbert	2017-11-25
\| *	In close_proof only check univ decls with the restricted context.	Gaëtan Gilbert	2017-11-24
\| *	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| *	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\|/