aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Fix #6591: anomaly when using selectors outside of a proof.Gravatar Cyprien Mangin2018-01-22
* Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
* Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\
* \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \
* | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* | | Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \
* \ \ \ Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
| | * | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | * | [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| | |/ /
* | / / Remove up-to-conversion matching functions.Gravatar Pierre-Marie Pédrot2017-12-09
| |/ / |/| |
| * | Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
|/ /
| * [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
* | Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
|/
* [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| * Make restrict_universe_context stronger.Gravatar Gaëtan Gilbert2017-11-25
| * In close_proof only check univ decls with the restricted context.Gravatar Gaëtan Gilbert2017-11-24
| * Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| * Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| * Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
* | [api] Remove 8.7 ML-deprecated functions.Gravatar Emilio Jesus Gallego Arias2017-11-07
| * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/
* Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Gravatar Maxime Dénès2017-11-06
|\
| * [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* | Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
|/
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
| * Cleanup suggest_bulletGravatar Gaëtan Gilbert2017-09-29
* | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Fix a refine anomaly "Evar defined twice".Gravatar Pierre-Marie Pédrot2017-09-06
* Merge PR #946: Functional pretyping interfaceGravatar Maxime Dénès2017-08-29
|\
* \ Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \
| | * Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
| |/ |/|
* | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* | | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26