Stream: Coq users

Topic: anomaly interp/impargs.ml

view this post on Zulip Eric Mark Martin (Sep 07 2021 at 23:51):

I'm trying to compile a CoFixpoint proof and when I try to step over the Qed I get

Error:
Anomaly
"File "interp/impargs.ml", line 378, characters 15-21: Assertion failed."

My collaborator on this project doesn't seem to get the same error. Any suggestions?

view this post on Zulip Ali Caglayan (Sep 08 2021 at 10:44):

What is your coq version?

view this post on Zulip Eric Mark Martin (Sep 09 2021 at 16:51):

coqtop --version gives me

The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 1 2021 17:50:25 with OCaml 4.12.0

view this post on Zulip Ali Caglayan (Sep 10 2021 at 12:32):

Is your collaborator using the same version? Also would you be able to reproduce the error in coqide and pass -bt so that we can get an ocaml backtrace, and get a better idea of whats going on.

Last updated: Oct 01 2023 at 18:01 UTC