aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* More comments in VM.Gravatar Maxime Dénès2016-10-19
* Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2016-10-12
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\
| * Fix for bug #4863, update the Proofview's env withGravatar Matthieu Sozeau2016-10-11
* | Removing a slow access to a named environment.Gravatar Pierre-Marie Pédrot2016-10-06
* | Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
|\ \
* \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-09
|\ \ \ | | |/ | |/|
| | * 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
| |/ |/|
* | Remove useless debug code.Gravatar Guillaume Melquiond2016-09-02
* | More efficient data structure to check if a native file is loaded.Gravatar Maxime Dénès2016-09-01
* | Use a better data structure for VM compilation of free vars.Gravatar Pierre-Marie Pédrot2016-08-22
* | 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
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
* | | Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* | | Please never mention .mli-only file in *.mllib (or future *.mlpack)Gravatar Pierre Letouzey2016-06-02
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \ | | |/ | |/|
| * | Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | | Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
| * | native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | | native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\| |
| * | Fixing an incompatility introduced in a404360: kernel conversion wasGravatar Hugo Herbelin2016-04-27
* | | This is an attempt to clarify terminology in choosing variable namesGravatar Hugo Herbelin2016-04-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:05:44 +0000