Pipeline · Iris / RefinedC

Fix cast insertion in the front end.

1 job for ci/frontent_fix in 14 minutes and 34 seconds (queued for 1 second)

Name Stage Failure

	Name	Stage	Failure
failed	build-coq.8.12.0	Build
	`File "./tutorial/proofs/t11_tree_set/generated_proof_remove.v", line 31, characters 2-6: Error: (in proof type_remove): Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. Makefile:6: recipe for target 'all_with_examples' failed make: *** [all_with_examples] Error 1 ERROR: Job failed: exit code 1`

failed

build-coq.8.12.0

Build



File "./tutorial/proofs/t11_tree_set/generated_proof_remove.v", line 31, characters 2-6:
Error:  (in proof type_remove): Attempt to save a proof with given up goals.
If this is really what you want to do, use Admitted in place of Qed.

Makefile:6: recipe for target 'all_with_examples' failed
make: *** [all_with_examples] Error 1
ERROR: Job failed: exit code 1