Fix DCE/Subst01 to work under lambdas (#1809) #358

Annotations

5 errors and 2 warnings

Makefile.coq:848: src/Coqprime/Tactic/Tactic.v

Makefile.coq.noex:848: /github/workspace/rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.v

Makefile.coq.noex:417: all

Makefile:68: noex

Makefile:87: bedrock2_noex

Could not find a terminator for warning: File "./src/coqutil/Datatypes/RecordSetters.v", line 410, characters 38-71: Warning: This expression should have type unit but has type bool. [not-unit,ltac2,default]

Could not find a terminator for warning: File "./src/coqutil/Datatypes/RecordSettersUsingExistingGetters.v", line 361, characters 38-71: Warning: This expression should have type unit but has type bool. [not-unit,ltac2,default]

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix DCE/Subst01 to work under lambdas (#1809) #358

docker-master

Fix DCE/Subst01 to work under lambdas (#1809) #358

Jobs

Run details

Annotations

The logs for this run have expired and are no longer available.

Re-running jobs...