aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
|\
| * [native comp] Improve error message on linking error.Gravatar Emilio Jesus Gallego Arias2017-01-26
* | Do not add redundant side effects in tactic code.Gravatar Pierre-Marie Pédrot2017-01-20
* | Mapping named_context_val preserves sharing when possible.Gravatar Pierre-Marie Pédrot2017-01-17
| * Handle application of a primitive projection to a not yet evaluated cofixpoin...Gravatar Guillaume Melquiond2016-12-26
* | Handle application of a primitive projection to a not yet evaluated cofixpoin...Gravatar Guillaume Melquiond2016-12-23
* | Fix #5248 - test-suite fails in 8.6beta1Gravatar Maxime Dénès2016-12-06
* | Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
|\ \
| * | Document changesGravatar Matthieu Sozeau2016-12-02
* | | Merge remote-tracking branch 'github/pr/377' into v8.6Gravatar Maxime Dénès2016-12-02
|\ \ \
* | | | Fix #5242 - Dubious unsilenceable warning on invalid identifierGravatar Maxime Dénès2016-12-02
| * | | Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
|/ / /
| * | Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
| * | Slightly more efficient [Univ.super] implemGravatar Matthieu Sozeau2016-11-30
|/ /
* | Fix incorrect long multiplication in the VM.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
|\|
| * Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 10:36:58 +0000