aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fix bug #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
* Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
* Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
* Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
* Add a few comments in term_typing.ml.Gravatar Maxime Dénès2017-03-21
* Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-21
* In the Kami project, that causes a stack overflow in one of the example filesGravatar Paul Steckler2017-03-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 20:05:25 +0000