aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
| | | * | | [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
| | | * | | Slightly more efficient [Univ.super] implemGravatar Matthieu Sozeau2016-11-30
| | |/ / /
| | * | | Fix incorrect long multiplication in the VM.Gravatar Guillaume Melquiond2016-11-24
* | | | | Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
|/ / / /
* | | | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\| |
* | | | COMMENT: Declarations.constant_defGravatar Matej Kosik2016-10-26
* | | | COMMENT: Names.Cmap and Names.Cmap_envGravatar Matej Kosik2016-10-26
* | | | COMMENT: Constr.kind_of_termGravatar Matej Kosik2016-10-26
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| | * | Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
| * | | More comments in VM.Gravatar Maxime Dénès2016-10-19
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\| | |
| * | | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2016-10-12
* | | | Merge branch 'v8.6'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 branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| | |
| * | | Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\ \ \
* | | | | UPDATE: reference to a deprecated variable "Filename.temp_dir_name" was repla...Gravatar Matej Kosik2016-09-29
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\| | | |
| * | | | 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
| | |/ / | |/| |
* | | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \ \
* \ \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ \ \ | | |/ / / | |/| | |