The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello,

While experimenting things on theories files I did not manage to
script files like this one:

theories/Classes/Morphisms.v

This looks like a bootstrapping problem of the rewrite tactic.

At line 364 I have this error:

respectful_morphism < rewrite <- H0.
    Toplevel input, characters 0-13:
> rewrite <- H0.
> ^^^^^^^^^^^^^
Error: Library Coq.Setoids.Setoid has to be required first.

Obviously the rewrite tactic called here is not he right one because
it depends on morphisms.

Running coqtop -boot does not solve the problem.

However:
coqtop -boot -compile theories/Classes/Morphisms.v
does compile the file (this is the way it is compiled when building coq).

Can someone tell me the correct coq invocation to start coqtop in
interactive mode on this file please?

Regards,
Pierre Courtieu