Andres Erbsen
Andres Erbsen
See also https://github.com/coq/coq/pull/827#issuecomment-333349523
If this project is successful to the best of our hopes, the maximal splitting (and perhaps ideal) that I see is as follows: - domain-specific provers from bedrock2 directory -...
Could you please elaborate on the extra work hinderance you see in keeping the parts that are currently together as they are?
Turns out `Load` isn't that easy either because paths ``` 130 andres-erbsen@andres-erbsen-sifive /tmp % find b :( b b/a.glob b/.a.aux b/a.v b/b.v andres-erbsen@andres-erbsen-sifive /tmp % coqc b/a.v File "./b/a.v", line...
I understand, but why is it in the word interface?
I think my main concern is that sextend does not seem like a natural word operation to me, in that its input is not clearly of the same type of...