ssreflect - importation de biblios ssreflect

Subject: Ssreflect Users Discussion List

List archive

importation de biblios ssreflect

From: Pierre Casteran <>
To:
Cc: Yves Bertot <>
Subject: importation de biblios ssreflect
Date: Thu, 04 Dec 2008 15:58:30 +0100

J'ai pu compiler Ssreflect sous trunk, mais je n'arrive pas à importer vers Coq une bibliothèque
comme par exemple paths.vo

Add LoadPath "/home/local/Ssreflect/theories".
Require Import paths.

Error: The file /home/local/Ssreflect/theories/paths.vo contains library
Ssreflect.paths and not library paths

Par ailleurs l'accès à la page

https://sympa.msr-inria.inria.fr//info/ssreflect

provoque une erreur 404

Pierre

importation de biblios ssreflect, Pierre Casteran, 12/04/2008
- Re: importation de biblios ssreflect, Assia Mahboubi, 12/04/2008
  - Re: importation de biblios ssreflect, Pierre Castéran, 12/04/2008
    - RE: importation de biblios ssreflect, Georges Gonthier, 12/04/2008

List archive

importation de biblios ssreflect