aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: remove dummy alias.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: module_kind to DeclaremodsGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
* Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\
* | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
| * Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* | [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
* | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
|/
* 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
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 18:08:04 +0000