aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2018-07-03Library: use ocaml typing to show that we find at most 2 filesGaëtan Gilbert
2018-07-03Library.register_loaded_library: remove unused variableGaëtan Gilbert
2018-07-03Libobject.apply_dyn_fun: remove unused deflt argumentGaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-18Remove reference name type.Maxime Dénès
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Pierre-Marie Pédrot
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: remove dummy alias.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: module_kind to DeclaremodsEmilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: multi to tactics/rewriteEmilio Jesus Gallego Arias
2018-06-01Merge PR #7234: Reduce circular dependency constants <-> projectionsMaxime Dénès
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-11Merge PR #7340: Remove DirClosedSection.Enrico Tassi
2018-05-11Merge PR #7341: Don't recurse into closed modules/sections in split_lib.Enrico Tassi
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-24Don't recurse into closed modules/sections in split_lib.Jasper Hugunin
2018-04-24Remove DirClosedSection.Jasper Hugunin
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
2018-04-06[api] Remove dependency of library on Vernacexpr.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-09Export the various option localities in the API.Pierre-Marie Pédrot
2018-03-07Use a proper warning when a summary is captured out of module scope.Vincent Laporte
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
2017-12-30Using a dedicated type for Lib.abstr_info.Pierre-Marie Pédrot
2017-12-22Merge PR #6469: No universe constraints in Let definitionsMaxime Dénès
2017-12-20Merge PR #6449: Let definitions must not contain side-effects when reaching t...Maxime Dénès
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
2017-12-18Merge PR #6284: Warning for absolute name masking (deprecated, should become ...Maxime Dénès
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
2017-12-14Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Maxime Dénès
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:40:52 +0000