The Coq mailing list

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

Thank you Hugo it works like a charm.
Regards,
Pierre

2012/9/3 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