Ssreflect Users Discussion List

["Pierre Castéran" <>]

Merci Assia,

 Juste un petit détail, et je fais mes essais demain.
 En fait, j'essayais d'importer depuis un fichier coq (donc compilé
avec coqc), le module paths de ssreflect. Donc je n'appelais pas
ssrcoq mais coqc avec un Require Import.

C'est donc dans le makefile  de mon développement que je dois ajouter
l'option -R ? Ou bien l'importation dans des fichiers coq "standard"
de définitions ssreflect est plus complexe que ça ?

A bientôt,

Pierre


> je suis tombée sur le même problème exactement hier. Ceci vient de  
> l'ajout d'une ligne -R ... dans la première ligne du fichier Make de  
> la contrib, que Jean-Marc a ajoutée. Je ne suis pas arrivée à la  
> supprimer mais je vais regarder. En attendant voici la réponse de  
> Jean-Marc Notin, à mon message lui signalant ce problème:
>
> ---
> En effet, je donne une systématiquement une option -R dans les  
> contrib, principalement pour la génération du html avec coqdoc  
> (sinon Coqdoc ne crée pas les bons liens...).
>
> Donc, pour que ça marche, il faut lancer ssrcoq avec -R :
>
>   ssrcoq -R /home/igg/magaud/Ssreflect/theories/ Ssreflect
>
> pour être cohérent avec les options de compilation.
>
> Voilà ! Normalement ça doit marcher :-)
> Tiens-moi au courant si ce n'est pas le cas...
> --
> Évidemment il faut remplacer /home/igg/magaud/ par le chemin vers le  
> répoertoire de la contrib Ssreflect chez toi :). Et je veux bien  
> aussi que tu me tiennes au courant si ceci ne résout pas au moins  
> temporairement ton problème...
>
> > Par ailleurs l'accès à la page
> >
> > https://sympa.msr-inria.inria.fr//info/ssreflect
> >
> > provoque une erreur 404
>
> Oups, merci de nous signaler ce problème, je regarde ça dès que  
> possible. Si tu as pu t'inscrire, je suppose que tu l'as fait en  
> envoyant un mail de souscription au serveur sympa?
>
> assia
>
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.



Pierre Castéran