search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
370 stars 79 forks source link

Make primitive arrays compile with todo "array" #1008

Closed mgbedmar closed 9 months ago

mgbedmar commented 10 months ago

The file Loader.v does not compile, it seems to be related with the compilation infrastructure but I haven't been able to solve it.

Also, mind file safechecker/theories/PCUICSafeRetyping.v, because it contains a todo (String.of_string "array"). I wasn't sure how to import files to avoid breaking everything.

@yforster @mattam82

mgbedmar commented 10 months ago

Just saw that there are new commits from Matthieu, let me rebase and I'll update the PR, sorry!

mgbedmar commented 10 months ago

Done.

mattam82 commented 10 months ago

I've pushed a branch which supports primitive arrays up-to the end of PCUIC for now (the rest should be relatively easy, I'll follow up on this next week).

Sorry I didn't see you rebased on it :) I'll start again from this then, thanks!

mattam82 commented 9 months ago

I reused some of this in the PR, closing now.