Adapt to coq PR #18921 fixing bugs of the inference of the return clause for Program-style pattern-matching #2748
Annotations
1 error and 10 warnings
|
Docker-Coq-Action
The RHS of Heq_x
|
|
Docker-Coq-Action
Notation map_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation app_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation rev_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation app_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation app_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation app_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation List.rev_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation List.rev_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation List.rev_length is deprecated since 8.20.
|
|
Docker-Coq-Action
Notation app_length is deprecated since 8.20.
|
Loading