Code

SProp#708

Code

Draft

yannl35133 wants to merge 17 commits intocoq-8.14MetaCoq/metacoq:coq-8.14from spropMetaCoq/metacoq:spropCopy head branch name to clipboard

+6,265-4,665

Commits

Commits on May 11, 2022

• Rebase relevance Template

  yannl35133

  committed
  edb57ee

  Copy full SHA for edb57ee

• Rebase relevance pcuic

  yannl35133

  committed
  ba7ef6c

  Copy full SHA for ba7ef6c

• First files of safechecker

  yannl35133

  committed
  09d673a

  Copy full SHA for 09d673a

• Relevance on terms

  yannl35133

  committed
  e7e08f8

  Copy full SHA for e7e08f8

Commits on May 17, 2022

• Compatibility between relevance from syntax and relevance from type

  yannl35133

  committed
  6bacff9

  Copy full SHA for 6bacff9

Commits on May 19, 2022

• Factor out admissions, safechecker

  yannl35133

  committed
  120be9d

  Copy full SHA for 120be9d

Commits on May 20, 2022

• Erasure

  yannl35133

  committed
  a6d7c5f

  Copy full SHA for a6d7c5f

Commits on May 23, 2022

• Add the missing file to PluginProject

  yannl35133

  committed
  477ea5d

  Copy full SHA for 477ea5d

• Add wf hypothesis to admitted lemmas

  yannl35133

  committed
  eeb7014

  Copy full SHA for eeb7014

Commits on May 24, 2022

• Make isTermRel an inductive predicate

  yannl35133

  committed
  761890a

  Copy full SHA for 761890a

• Plugin fix

  yannl35133

  committed
  dfaf094

  Copy full SHA for dfaf094

• Fill the auxilliary lemmas about the relevance of constructors/inductives

  mattam82

  committed
  4c38291

  Copy full SHA for 4c38291

Commits on May 25, 2022

• Fill the proof for projections as well

  mattam82

  committed
  5162310

  Copy full SHA for 5162310

• Adapt to new projection_type(_and_eq) lemmas

  mattam82

  committed
  ea6493a

  Copy full SHA for ea6493a

Commits on May 26, 2022

• Move lemmas to their right place

  mattam82

  committed
  35cd102

  Copy full SHA for 35cd102

Commits on Jun 10, 2022

• Replace typ_or_sort with a judgment type (binary or ternary with options)

  yannl35133

  committed
  c2699f9

  Copy full SHA for c2699f9

Commits on Jul 5, 2022

• Prepare for rebase

  yannl35133

  committed
  6adeff3

  Copy full SHA for 6adeff3