MetaCoq CI

Prove that dearging preserves eta-expanded constructors and fixpoints… #2565

Annotations

1 error and 10 warnings

Unable to apply lemma of type "forall x y : ?A, x == y -> x = y"

The default and global localities for this command outside sections

Notation "_ { _ := _ }" was already used.

Notation "_ ,,, _" was already used.

Notation "_ * _" was already used in scope type_scope.

Notation "_ <-> _" was already used in scope type_scope.

Notation "_ + _" was already used in scope type_scope.

Notation "_ * _" was already used in scope type_scope.

Notation "_ <-> _" was already used in scope type_scope.

Notation "_ + _" was already used in scope type_scope.

Use of “Require” inside a section is fragile. It is not recommended