The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Pierre,

I guess that what you are looking for is 

  coqtop -top Coq.Classes.Morphisms

This sets the toplevel module name to be "Coq.Classes.Morphisms"
instead of the default "Top". Then, the lemmas defined in Morphisms
and referred to with their expected qualified name in the setoid
rewriting tactic, which itself is called from Morphisms.v, will be
correctly identified (when using "Load Morphisms").

Hugo

On Mon, Sep 03, 2012 at 05:13:03PM +0200, Pierre Courtieu wrote:
> 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