Enzo Crance

coq.env.add-indt fails to add universe polymorphic inductives when not in a section

2

Declaring a new universe polymorphic inductive type with `coq.env.add-indt` fails when not in a section. ```coq From elpi Require Import elpi. Set Universe Polymorphism. Elpi Tactic test. (* Section Test....

Failure of coq.env.add-indt in the presence of non uniform parameters

3

Here is an inductive type: ```coq Inductive t (n : nat) : Type := | K : t O -> t n. ``` Here is its parametricity translation built in...

The term manipulation API functions like `fold-map` or `copy` are untyped, *i.e.*, they traverse binders adding untyped bound variables with `pi x` instead of using `@pi-decl ...`. As discussed, maybe...

:sparkles: Add coq.univ.super

6

Short utility function to make `Type@{i+1}`

Pair equality handling

2

Hello. I am planning to use **zify** / **mczify** as a source of inspiration for a pre-processing tool whose purpose is to prepare Coq goals before their translation to the...