Search results

indices of inductives need to be named

Status: Open.

#12 In aa755/paramcoq-iff;

· aa755 opened on Aug 7, 2017

automatic translation of dependencies

enhancement

Status: Open.

#11 In aa755/paramcoq-iff;

· aa755 opened on Jul 26, 2017

Coq's representation of match branches

Status: Open.

#9 In aa755/paramcoq-iff;

· aa755 opened on May 4, 2017

recursively non-uniform parameters of inductive types

Status: Open.

#8 In aa755/paramcoq-iff;

· aa755 opened on Apr 25, 2017

preprocess to remove shadowing of bvars

Status: Open.

#7 In aa755/paramcoq-iff;

· aa755 opened on Apr 21, 2017

higher universes

enhancement

Status: Open.

#6 In aa755/paramcoq-iff;

· aa755 opened on Apr 4, 2017

nested inductives

enhancement

Status: Open.

#5 In aa755/paramcoq-iff;

· aa755 opened on Apr 4, 2017

extraction to an (OCaml) plugin for Coq

enhancement

Status: Open.

#4 In aa755/paramcoq-iff;

· aa755 opened on Mar 22, 2017

test on standard library, well-founded Functions.

enhancement

Status: Open.

#3 In aa755/paramcoq-iff;

· aa755 opened on Mar 22, 2017

too slow

enhancement

Status: Open.

#2 In aa755/paramcoq-iff;

· aa755 opened on Mar 22, 2017