Code

Port fix-to-elim to Coq 8.11#15

Code

Draft

InnovativeInventor wants to merge 17 commits intomasteruwplse/fix-to-elim:masterfrom 8.11uwplse/fix-to-elim:8.11Copy head branch name to clipboard

+27-22

Commits

Commits on Aug 2, 2022

• Port fixtranslation to mlg

  InnovativeInventor

  committed
  184ac21

  Copy full SHA for 184ac21

Commits on Aug 20, 2022

• Remove unused imports

  InnovativeInventor

  committed
  d5fb340

  Copy full SHA for d5fb340

• Mark certain warnings as non-fatal

  InnovativeInventor

  committed
  1a6e185

  Copy full SHA for 1a6e185

• Port desugar to Coq 8.11

  InnovativeInventor

  committed
  242389a

  Copy full SHA for 242389a

• Finish porting fix-to-elim to 8.11

  InnovativeInventor

  committed
  00a0d7a

  Copy full SHA for 00a0d7a

• Ignore autogenerated files

  InnovativeInventor

  committed
  f458a3d

  Copy full SHA for f458a3d

• Add back seemingly unnecessary imports

  InnovativeInventor

  committed
  dc1f449

  Copy full SHA for dc1f449

Commits on Aug 22, 2022

• Fix desugar_constr bug (need to return term, not type)

  InnovativeInventor

  committed
  7ee9017

  Copy full SHA for 7ee9017

Commits on Aug 23, 2022

• Add set -euxo pipefail so tests halt at first failure

  InnovativeInventor

  committed
  1aaffb3

  Copy full SHA for 1aaffb3

• Pass env to transform_module_structure

  InnovativeInventor

  committed
  51078f8

  Copy full SHA for 51078f8

Commits on Sep 27, 2022

• Fix regression issue (do not refresh env!)

  InnovativeInventor

  committed
  52d3261

  Copy full SHA for 52d3261

• Update coq-plugin-lib version

  InnovativeInventor

  committed
  b15e64d

  Copy full SHA for b15e64d

Commits on Oct 3, 2022

• Bump coq-plugin-lib submodule commit

  InnovativeInventor

  committed
  03b744b

  Copy full SHA for 03b744b

• Update coq-plugin-lib submodule

  InnovativeInventor

  committed
  e5b90f6

  Copy full SHA for e5b90f6

• Update coq-plugin-lib submodule

  InnovativeInventor

  committed
  d2561ae

  Copy full SHA for d2561ae

• Reorder imports in mlpack

  InnovativeInventor

  committed
  31a2102

  Copy full SHA for 31a2102

Commits on Nov 3, 2022

• Update coq-plugin-lib submodule

  InnovativeInventor

  committed
  65e997f

  Copy full SHA for 65e997f