Code

Merge 8.16 in 8.14#727

Code

Merged

mattam82 merged 12 commits intocoq-8.14MetaCoq/metacoq:coq-8.14from merge-8.16-in-8.14MetaCoq/metacoq:merge-8.16-in-8.14Copy head branch name to clipboardJul 1, 2022

+6,472-783

Commits

Commits on Jul 1, 2022

• Replace all uses of todo and Admitted by axioms (#717)

  Show description for 488ac9d
  

  yforster

  and

  mattam82

  committed
  488ac9d

  Copy full SHA for 488ac9d

• Ensure constant constructors are declared in evaluation (#718)

  mattam82

  committed
  b6daf8c

  Copy full SHA for b6daf8c

• Update readmes (#719)

  Show description for 17b9492
  mattam82

  committed
  17b9492

  Copy full SHA for 17b9492

• Fix README

  mattam82

  committed
  a247fa6

  Copy full SHA for a247fa6

• Remove warnings (#720)

  Show description for f8510b0
  

  yforster

  authored and

  mattam82

  committed
  f8510b0

  Copy full SHA for f8510b0

• Constructor tactic example (#725)

  mattam82

  committed
  78b5df8

  Copy full SHA for 78b5df8

• Constructors as blocks (#723)

  Show description for 5b410f1
  

  mattam82

  and

  yforster

  committed
  5b410f1

  Copy full SHA for 5b410f1

• [doc] Update erasure README.md for constructors-as-blocks

  mattam82

  committed
  1f45662

  Copy full SHA for 1f45662

• Update README.md and self_erasure file

  mattam82

  committed
  7fde2fb

  Copy full SHA for 7fde2fb

• Update DOC.md and dependency graph

  mattam82

  committed
  0102668

  Copy full SHA for 0102668

• Point to 8.14 branch in README

  mattam82

  committed
  d921719

  Copy full SHA for d921719

• Fixes after merge

  mattam82

  committed
  c97d948

  Copy full SHA for c97d948