aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* 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
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Merge PR #1114: Generic handling of nameable objects for pluginsGravatar Maxime Dénès2017-10-09
|\
* | [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
| * Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
* | Removing now useless former fix to #3333 (check valid module names).Gravatar Hugo Herbelin2017-09-12
|/
* Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\
* \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \
| | * Canonically renaming fold_map into fold_left_map in library Name.Gravatar Hugo Herbelin2017-08-29
| |/ |/|
* | Print names of all open blocksGravatar Tej Chajed2017-08-06
| * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
|/