Code

Support primitive array terms#998

Code

Merged

mattam82 merged 17 commits intocoq-8.17MetaCoq/metacoq:coq-8.17from primitive-arraysMetaCoq/metacoq:primitive-arraysCopy head branch name to clipboardNov 30, 2023

+4,209-824

Commits

Commits on Nov 24, 2023

• Support primitive array terms

  mattam82

  committed
  4566665

  Copy full SHA for 4566665

• WIP up to confluence for arrays

  mattam82

  committed
  ed544ea

  Copy full SHA for ed544ea

• Alpha-conv and validity done

  mattam82

  committed
  c86a3a8

  Copy full SHA for c86a3a8

• Proved subject reduction for arrays

  mattam82

  committed
  26779c7

  Copy full SHA for 26779c7

• Adapted all of PCUIC to primitive arrays (and in general term containers in primitives)

  mattam82

  committed
  a7af745

  Copy full SHA for a7af745

• Done with template <-> PCUIC. Working on safe checker

  mattam82

  committed
  e93c39c

  Copy full SHA for e93c39c

• Update PCUICPosition to include arrays

  mattam82

  committed
  3ee01a3

  Copy full SHA for 3ee01a3

• Updatet SafeConversion to arrays

  mattam82

  committed
  67bba98

  Copy full SHA for 67bba98

• Typechecking of arrays

  mattam82

  committed
  51cb57d

  Copy full SHA for 51cb57d

• In erasure, must update solve_all to automate proofs

  mattam82

  committed
  69c1f05

  Copy full SHA for 69c1f05

• WIP in erasure of arrays

  mattam82

  committed
  8ecbd0e

  Copy full SHA for 8ecbd0e

• Adapt erasure for primitive arrays

  mattam82

  committed
  3354847

  Copy full SHA for 3354847

• Disable quotation module build

  mattam82

  committed
  8b4d7a9

  Copy full SHA for 8b4d7a9

• Fixes after rebase

  mattam82

  committed
  133b5ad

  Copy full SHA for 133b5ad

Commits on Nov 30, 2023

• Fix translations, and a bit of quotation, up-to an issue with nested

  Show description for 8b5049f
  mattam82

  committed
  8b5049f

  Copy full SHA for 8b5049f

• Disable quotation opam module dependency

  mattam82

  committed
  1dd8994

  Copy full SHA for 1dd8994

• Disable the opam quotation package for now

  mattam82

  committed
  7dd6de8

  Copy full SHA for 7dd6de8