aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules
Commit message (Expand)AuthorAge
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* MAJ syntaxe v7 avant activation en syntaxe v8Gravatar herbelin2005-12-21
* Anciennement déplacé dans 'output'Gravatar herbelin2005-12-21
* Simplest Demo on modulesGravatar coq2003-11-28
* L'exemple phare de modules - simplifie pour TPHOLsGravatar coq2003-09-22
* Corrige Bug (PR#290)Gravatar coq2003-05-05
* commentaireGravatar coq2003-02-06
* MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutGravatar coq2003-01-31
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-11-24
* Encore quelques rangements dans Nametab + petits trucsGravatar coq2002-09-27
* Encore quelques tests sur modules...Gravatar coq2002-08-16
* Petites corrections ici et laGravatar coq2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02