I managed to get
File "/tmp/tmpmop1bru0/Crypto/Assembly/Symbolic.v", line 543, characters 0-9:
Error: Anomaly "in Lemmas.save_lemma_admitted: more than one statement."
Please report at http://coq.inria.fr/bugs/.
while minimizing https://github.com/coq/coq/issues/16834 here. Any guesses about the cause? (I can try to track it down on my own later, but it'll be a bit annoying, and if anyone can guess a way to trigger it, that'd save me some work.)
Reported at https://github.com/coq/coq/issues/16856, not yet minimized
Answer: Admitted
doesn't work with Derive
Last updated: May 31 2023 at 16:01 UTC