aa755/paramcoq-iff

Issues

• preprocess to remove shadowing of bvars

  #7 opened 8 years ago by aa755
  1

• indices of inductives need to be named

  #12 opened 7 years ago by aa755
  0

• automatic translation of dependencies

  #11 opened 7 years ago by aa755
  0

• Coq's representation of match branches

  #9 opened 8 years ago by aa755
  0

• recursively non-uniform parameters of inductive types

  #8 opened 8 years ago by aa755
  0

• higher universes

  #6 opened 8 years ago by aa755
  0

• nested inductives

  #5 opened 8 years ago by aa755
  0

• extraction to an (OCaml) plugin for Coq

  #4 opened 8 years ago by aa755
  0

• test on standard library, well-founded Functions.

  #3 opened 8 years ago by aa755
  0

• too slow

  #2 opened 8 years ago by aa755
  0

• too slow.

  #1 opened 8 years ago by aa755
  0