Stream: Coq devs & plugin devs

Topic: dev/shim/coqtop inconsistent assumptions


view this post on Zulip Jason Gross (Sep 11 2023 at 16:01):

How do I fix this error?

$ dune exec -- dev/shim/coqtop
Welcome to Coq JasonGross-X1:/home/jgross/Documents/GitHub/coq/_build/default,more-float-tests (8ab822058e182da36e3b77a764cd5b38cb728ed6)

Coq < From Coq Require Import Strings.
Toplevel input, characters 0-32:
> From Coq Require Import Strings.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path
Strings with prefix Coq.

Coq < From Coq Require Import String.
Toplevel input, characters 0-31:
> From Coq Require Import String.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
Compiled library Coq.Strings.String (in file /home/jgross/Documents/GitHub/coq/_build/default/theories/Strings/String.vo) makes inconsistent assumptions over library Coq.Init.Ltac

Coq <

Last updated: Oct 13 2024 at 01:02 UTC