Search results

More general handling of identity / composition for relators

Status: Open.

#17 In CertiKOS/coqrel;

· jeremie-koenig opened on Oct 16, 2018

Default Equivalence instance should be for (=) not ⊤

Status: Open.

#16 In CertiKOS/coqrel;

· jeremie-koenig opened on May 30, 2018

Sort out header levels in Coqdoc

Status: Open.

#13 In CertiKOS/coqrel;

· jeremie-koenig opened on Jan 28, 2017

opam package

Status: Open.

#11 In CertiKOS/coqrel;

· vzaliva opened on Jan 21, 2017

Investigate a leftward arrow

enhancement

Status: Open.

#8 In CertiKOS/coqrel;

· jeremie-koenig opened on Aug 19, 2016

Rewriting becomes very slow under certain circumstances

Status: Open.

#6 In CertiKOS/coqrel;

· jwiegley opened on Aug 9, 2016

Add a <code>Relational Scheme</code> command for deriving relators from inductive type definitions

enhancement

Status: Open.

#1 In CertiKOS/coqrel;

· jeremie-koenig opened on Jan 27, 2016