aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
Commit message (Expand)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [econstr] Remove some Unsafe.to_constr use.Gravatar Emilio Jesus Gallego Arias2018-06-04
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Cosmetic: add an expected newline in proof_global.Gravatar Hugo Herbelin2018-03-08
* Rename some universe minimizing "normalize" functions to "minimize"Gravatar Gaëtan Gilbert2018-03-06
* Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* 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
* Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
* 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
* 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] 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
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
* Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* | Remove Warnings: unused value ...Gravatar Amin Timany2017-06-16
* | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| * [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
|/
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * | Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
| |\ \ | | |/ | |/|
| | * [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * | Change wrong bullet message.Gravatar Théo Zimmermann2017-05-20
| |/
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge PR#552: Miscelaneous commitsGravatar Maxime Dénès2017-04-24
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 16:34:24 +0000