aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
| | | * | Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| | * | | Restore native compiler optimizations after they were broken by 9e2ee58.Gravatar Maxime Dénès2016-09-09
| | | * | Removing the now useless field env_named_val from named_context_val.Gravatar Pierre-Marie Pédrot2016-09-09
| | | * | More efficient implementation of map_named_val.Gravatar Pierre-Marie Pédrot2016-09-09
| | | * | Fast access environment in CClosure.Gravatar Pierre-Marie Pédrot2016-09-09
| | | * | Tentative fast-access named envGravatar Pierre-Marie Pédrot2016-09-09
| | | * | Packing the named_context_val in a proper record and marking it private.Gravatar Pierre-Marie Pédrot2016-09-09
| | |/ / | |/| |
* | | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \ \
* \ \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Remove useless debug code.Gravatar Guillaume Melquiond2016-09-02
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| | | |
| * | | | More efficient data structure to check if a native file is loaded.Gravatar Maxime Dénès2016-09-01
* | | | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | | | CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which...Gravatar Matej Kosik2016-08-26
* | | | | CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...Gravatar Matej Kosik2016-08-26
* | | | | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* | | | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| | | |
* | | | | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
* | | | | CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* | | | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | | | Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
* | | | | Merging a branch that adds "Context.Named.Declaration.to_rel" function.Gravatar Matej Kosik2016-08-24
|\ \ \ \ \
| * | | | | Adding "Context.Named.Declaration.to_rel" functionGravatar Matej Kosik2016-08-24
| | * | | | Use a better data structure for VM compilation of free vars.Gravatar Pierre-Marie Pédrot2016-08-22
| | | * | | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | * | | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ / / |/| | | |
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\ \ \ \ \ | | |/ / / | |/| | |
* | | | | Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_t...Gravatar Pierre-Marie Pédrot2016-08-17
| |/ / / |/| | |
* | | | Adding "Context.Named.Declaraton.of_rel" functionGravatar Matej Kosik2016-08-11
* | | | CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" fu...Gravatar Matej Kosik2016-08-11
* | | | CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" fu...Gravatar Matej Kosik2016-08-11
| * | | Make code a bit clearer by removing optional argument.Gravatar Guillaume Melquiond2016-08-10
|/ / /
* | | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\| |
| * | Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\| |
| * | Prevent unsafe overwriting of Required modules by toplevel library.Gravatar Maxime Dénès2016-07-05
| * | congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
* | | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* | | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
* | | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
* | | Fix bug #4825: [clear] should not dependency-check hypotheses that come above...Gravatar Pierre-Marie Pédrot2016-06-20
* | | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* | | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | | Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
* | | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | | Adding a default safe set of kernel typing flags to Declareops.Gravatar Pierre-Marie Pédrot2016-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 07:20:15 +0000