Matthieu Sozeau
Matthieu Sozeau
Ah yes, I know how to fix it
@SkySkimmer This should be fixed now, can you check?
Could it be that opam is confused because the parent directory (user-contrib) gets modified by other Coq contribs?
Hmm, we should use a Module then.
@andrew-appel you might have some information I don't have here?
We now have a choice of either 8.18 or 8.19. I guess the later, which will be available everywhere soonish.
We'll switch to 8.19 now that it's released and a platform is comming for it.
(Unsigned) Int63 are translated to immediate ints, just like in ocaml. We verify the basic operational semantics: if something evaluates to a primitive int in Coq, it evaluates to the...
Any hope to make a quick and dirty search/searchabout available? Even when writting `Search foo` in the document I don't see any result. It's kind of crucial to work on...
Ah I see, it was just after the statement