Code

Add trans_one_inductive_entry#789

Code

Merged

mattam82 merged 6 commits intoMetaCoq:coq-8.16MetaCoq/metacoq:coq-8.16from JasonGross:trans_one_inductive_entryJasonGross/metacoq:trans_one_inductive_entryCopy head branch name to clipboardDec 15, 2022

+87-73

Commits

Commits on Nov 28, 2022

• Add trans_one_inductive_entry

  JasonGross

  committed
  f42928b

• Add a comment with a partial trans_mutual_inductive_entry

  JasonGross

  committed
  581badb

• Move PCUIC AST entries down

  Show description for c9f5878
  JasonGross

  committed
  c9f5878

Commits on Nov 29, 2022

• Use context in PCUICAst.mutual_inductive_entry

  JasonGross

  committed
  380690d

• Finish trans_mutual_inductive_entry

  JasonGross

  committed
  496e55c

Commits on Dec 6, 2022

• Add TODOs to PCUICToTemplate

  JasonGross

  authored
  e4f085f