| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix #6677: Critical bug with VM and universes |  Maxime Dénès | 2018-02-12 |
| | | | | | | | This bug was present since the first patch adding universe polymorphism handling in the VM (Coq 8.5). Note that unsoundness can probably be observed even without universe polymorphism. | ||
| * | Safer VM interfaces | Maxime Dénès | 2018-01-26 |
| We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |