Nicolas Tabareau

Quoting does not work on the following defintion ``` Class Canonical_eq (A:Type) := { can_eq : forall (x y : A), x = y -> x = y ; can_eq_refl...

### Description of the problem the sort of the equality used to discriminate should be the same as the sort of the goal. ### Small Coq file to reproduce the...

discriminate and injection do not work with sort polymorphic inductive types

1

### Description of the problem the `discriminate` and `injection` tactics are not compatible with sort polymorphic inductive types instantiated at `Type` ### Small Coq file to reproduce the bug ```coq...

When a sort poly constant is translated, the sort variable is not propagated and thus substituted with Type instead. Given that the names of universe level change also, I suspect...

Problem with translating terms using SProp

1

``` Definition Has_Leibniz (eq : forall A : Type, A -> A -> Prop) := forall (A : Type) (x : A) (P : A -> SProp), P x ->...