coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6874: [econstr] Some minor tweaks	Pierre-Marie Pédrot	2018-06-07
\|\
\| *	[econstr] Remove some Unsafe.to_constr use.	Emilio Jesus Gallego Arias	2018-06-04
* \|	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
\|/
*	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...	Pierre-Marie Pédrot	2018-05-24
\|\
\| *	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
\| *	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
* \|	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias	2018-05-23
\|/
*	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
*	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
\|/ /