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
Admitted doesn't work with
Last updated: Dec 07 2023 at 06:38 UTC