aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-05-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 85f007b7-540e-04...soubiran
2007-02-21Removed some useless code in mod_typing that was redundant with safe_typing.soubiran
2007-01-19Prise en compte des univers algébriques dans les types inférés dansherbelin
2007-01-17Correction bug #1302herbelin
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans injection...jforest
2006-10-17Clarification des contraintes sur le contexte de paramètres desherbelin
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
2006-09-14Correction du bug #1181jforest
2006-05-10Conformité nouveaux principes: Declare Module non utilisable pour définir u...herbelin
2006-04-15Test synchronisation chargement objets non logiquesherbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2005-12-21MAJ syntaxe v7 avant activation en syntaxe v8herbelin
2005-12-21Anciennement déplacé dans 'output'herbelin
2003-11-28Simplest Demo on modulescoq
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
2003-05-05Corrige Bug (PR#290)coq
2003-02-06commentairecoq
2003-01-31MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutcoq
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-08-16Encore quelques tests sur modules...coq
2002-08-13Petites corrections ici et lacoq
2002-08-02Modules dans COQ\!\!\!\!coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:51:21 +0000