aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-28Simplest Demo on modulescoq
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
2003-11-25CC: added injection theorycorbinea
2003-11-13Niveau V8herbelin
2003-11-13Fermeture de la section maintenant necessaireherbelin
2003-11-13Passage a un SStream predicatifherbelin
2003-11-09Test Generalizeherbelin
2003-10-27MAJherbelin
2003-10-14Test obsoleteherbelin
2003-10-13Cleaningherbelin
2003-10-11Logic_TypeSyntax disparuherbelin
2003-10-10*** empty log message ***herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-10Cacher les .v8herbelin
2003-10-08Teste interaction ltac et modulesherbelin
2003-10-08Ajout exemple parametres implicitesherbelin
2003-10-08Test Conjectureherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-02Traduction des tests success et test en v8herbelin
2003-09-23Correction bug 328coq
2003-09-23test d'implicite incorrect depuis que eq porte sur Typebarras
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
2003-09-06Check local definitions in context of inductive typesherbelin
2003-09-03Projectionsherbelin
2003-06-21Added a test for Functional Induction.courtieu
2003-05-22Test backtrackingherbelin
2003-05-21Nouveaux testsherbelin
2003-05-05Corrige Bug (PR#290)coq
2003-04-27Ce que Try récupèreherbelin
2003-04-15Débranchement des tests output qui sont faussés par le traducteurherbelin
2003-03-29indentationherbelin
2003-03-14*** empty log message ***barras
2003-03-04MAJherbelin
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
2003-02-27Adding tests for the "functional induction" facility.bertot
2003-02-06commentairecoq
2003-01-31MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutcoq
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
2003-01-28MAJ pour Regdesmettr
2003-01-22*** empty log message ***barras
2003-01-20*** empty log message ***herbelin
2003-01-19Tests ltacherbelin
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
2003-01-16*** empty log message ***herbelin
2003-01-15Problème de désynchronisation des variables du type et du corps d'un point-...herbelin
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...herbelin
2003-01-09Export M + Module M <: SIGcoq
2002-12-12Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...desmettr
2002-12-09Add an example with Ring.bertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:35:00 +0000