aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\
* \ Merge PR #7340: Remove DirClosedSection.Gravatar Enrico Tassi2018-05-11
|\ \
* \ \ Merge PR #7341: Don't recurse into closed modules/sections in split_lib.Gravatar Enrico Tassi2018-05-11
|\ \ \
| | | * [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
| |_|/ |/| |
* | | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| * | Don't recurse into closed modules/sections in split_lib.Gravatar Jasper Hugunin2018-04-24
|/ /
| * Remove DirClosedSection.Gravatar Jasper Hugunin2018-04-24
|/
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
* [api] Remove dependency of library on Vernacexpr.Gravatar Emilio Jesus Gallego Arias2018-04-06
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
| * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* | Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
* | Export the various option localities in the API.Gravatar Pierre-Marie Pédrot2018-03-09
|/
* Use a proper warning when a summary is captured out of module scope.Gravatar Vincent Laporte2018-03-07
* 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
* Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* Using a dedicated type for Lib.abstr_info.Gravatar Pierre-Marie Pédrot2017-12-30
* Merge PR #6469: No universe constraints in Let definitionsGravatar Maxime Dénès2017-12-22
|\
* \ Merge PR #6449: Let definitions must not contain side-effects when reaching t...Gravatar Maxime Dénès2017-12-20
|\ \
| | * Let definitions do not create new universe constraints.Gravatar Pierre-Marie Pédrot2017-12-19
| | * Specific type for section definition entries.Gravatar Pierre-Marie Pédrot2017-12-19
| |/
* | Merge PR #6284: Warning for absolute name masking (deprecated, should become ...Gravatar Maxime Dénès2017-12-18
|\ \
| | * Let definitions must not contain side-effects when reaching the kernel.Gravatar Pierre-Marie Pédrot2017-12-16
| |/ |/|
* | Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6275: [summary] Allow typed projections from global state.Gravatar Maxime Dénès2017-12-12
|\ \ \
* | | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| * | | [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
| * | | [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/ / /
| * | [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
* | | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
|/ /
* | Merge PR #1049: Remove obsolete localityGravatar Maxime Dénès2017-11-30
|\ \
| | * Warning for absolute name masking (making it deprecated, should becomeGravatar Matthieu Sozeau2017-11-30
| * | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| |/
* / [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
|/
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [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
|\
* \ Merge PR #6065: [api] Deprecate all legacy uses of Names in 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
| |/
| * [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:13:07 +0000