Clément Blaudeau

Another way of exploiting this overabstraction is to use the invalid signature inferred as an argument of a functor (using `module type of`), which leads to (through, I believe, path...

Inside the body of a functor, the user cannot build a module that the typechecker accepts as an alias to the argument, so a module type featuring such alias is...

Which can be made even simpler: ```ocaml module type T module F = functor (Y : T) (Alias : sig module X' = Y end) -> Alias;; (* module F...

As pointed out by @gasche and @lpw25, one can use this to build a functor that outputs an alias to its argument, which I believe is unsound ? A minimal...

Just for reference, I found a smaller example that also crashes the typechecker: ```ocaml module F (Type: sig module type T end)(Y:Type.T) = Y module Crash (Y:sig end) = F(struct...

Do you reuse the subtyping check of first-class modules ? ```Type (module Functor) is not compatible with type (module Applicative)``` This looks like the type of the first-class module `(module...

Hi Sam, Thank you for you answer. I don't see any errors when running emacs alone (`emacs --debug-init` does not output anything). The result of `M-x emacs-version` is ``` GNU...

I've managed to get it (half) working on Fedora by : 1. Adding the `-q` option in the `install.sh` file (line 39) 2. Using the patch [pvs-emacs.zip](https://github.com/SRI-CSL/PVS/files/15419080/pvs-emacs.zip) (re-attached here as...