aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Merge PR#519: Faster side effectsGravatar Maxime Dénès2017-04-07
|\
| * Inline the only use of hcons_j in Term_typing.Gravatar Pierre-Marie Pédrot2017-04-07
| * Documenting the fact terms are only hashconsed outside of a section.Gravatar Pierre-Marie Pédrot2017-04-06
* | Merge PR#434: Optimizing array mapping in the kernel.Gravatar Maxime Dénès2017-04-05
|\ \
| | * More efficient check in validity of side-effects.Gravatar Pierre-Marie Pédrot2017-03-27
| | * Adding the size of the opaquetab in its representation.Gravatar Pierre-Marie Pédrot2017-03-27
| | * Fix hashconsing of terms in the kernel.Gravatar Pierre-Marie Pédrot2017-03-27
| |/ |/|
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
|\ \
| * | 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
* | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\ \ \
* \ \ \ Merge PR#482: [toplevel] Remove unusable option -notopGravatar Maxime Dénès2017-03-22
|\ \ \ \
| | | * | 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
| | |/ /
* | | | Merge PR#134: Enable `-safe-string`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
| * | | | [misc] Remove warnings about String.setGravatar Emilio Jesus Gallego Arias2017-03-20
| * | | | [safe-string] Enable -safe-string !Gravatar Emilio Jesus Gallego Arias2017-03-14
| * | | | [safe_string] library/nameopsGravatar Emilio Jesus Gallego Arias2017-03-14
| * | | | [safe_string] kernel/cemitcodesGravatar Emilio Jesus Gallego Arias2017-03-14
| | * | | [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
| * | | | [safe-string] kernel/nativevaluesGravatar Emilio Jesus Gallego Arias2017-03-14
| * | | | [safe_string] kernel/term_typingGravatar Emilio Jesus Gallego Arias2017-03-14
| |/ / /
* / / / [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
|/ / /
* | | Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
|\ \ \
| | | * Optimizing array mapping in the kernel.Gravatar Pierre-Marie Pédrot2017-02-19
| | |/
* | | Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
| |\ \ \
| | | * | Remove useless commentsGravatar Gaetan Gilbert2017-01-28
| | * | | [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
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\| | | |
| * | | | 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
* | | | | Fixing injection in the presence of let-in in constructors.Gravatar Hugo Herbelin2016-12-22
| | | * | Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
| | | * | Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
| |_|/ / |/| | |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\| | |
| * | | 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
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\| | | | |
| | * | | | Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
| |/ / / /
| | * | | Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30