aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\
| * Remove reference name type.Gravatar Maxime Dénès2018-06-18
* | Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/
* Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Gravatar Pierre-Marie Pédrot2018-06-14
|\
* | [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
| * Fixes #7192 (Print Assumptions does not enter implementation of submodules).Gravatar Hugo Herbelin2018-04-07
* | [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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 17:11:55 +0000