Clément Blaudeau
Clément Blaudeau
### Overview Generally, inside the signature of the body of a functor, aliases involving the functor's argument are not allowed (for soundness reasons). However, they seems to be authorized inside...
Hi, The Ocaml typechecker (overly) abstracts module types when they contain types equalities that cannot be expressed. This leads to invalid signatures being inferred. A minimal example is the following...
### Overview When writing a module type of a functor where the argument has internal aliases (between some of its submodules), OCaml accepts the module type while silently removing those...
### Overview (Might be similar to https://github.com/ocaml/ocaml/issues/11441 ?) Generally, inside the signature of the body of a functor, aliases involving the functor's argument are not allowed (for soundness reasons). However,...
Dear PVS developpers, While trying to install the latest version (or any recent snapshot), I have an error when running `./install-sh` : `!!! Something went wrong - see the end...
When working with datatypes, and writing theorems involving subterms, I often have to carefully expand `subterm` at precise positions in my proofs, which make them less automated and more fragile....
When defining a recursive module with a signature that contains a module type substitution, the substituted module type is not properly checked. This leads to cyclic definitions that makes the...
This issue is in two parts, and was discovered by investigating [this bug with recursive modules](https://discuss.ocaml.org/t/recursive-module-inside-functor/14575/5) ## Loss of applicativity with submodules First, the applicativity of functors can be broken...
When defining a functor that takes an abstract module type as input, applications of that functor do not get strengthened after the abstract module type has been resolved to a...