aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28Simplest Demo on modulescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25CC: added injection theorycorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Niveau V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Fermeture de la section maintenant necessaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4893 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Passage a un SStream predicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4891 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Test Generalizeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4837 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4718 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Test obsoleteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4634 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Cleaningherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4616 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Logic_TypeSyntax disparuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4558 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Teste interaction ltac et modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4552 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Ajout exemple parametres implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4551 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Test Conjectureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4545 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Traduction des tests success et test en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4514 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Correction bug 328coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4456 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23test d'implicite incorrect depuis que eq porte sur Typebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4455 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4449 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Check local definitions in context of inductive typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4323 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4298 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-21Added a test for Functional Induction.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4195 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Test backtrackingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4062 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Nouveaux testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-05Corrige Bug (PR#290)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3989 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-27Ce que Try récupèreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3960 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-15Débranchement des tests output qui sont faussés par le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3925 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29indentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3811 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3731 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Adding tests for the "functional induction" facility.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-06commentairecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3667 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3635 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28MAJ pour Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3596 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3547 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Tests ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3539 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3516 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Problème de désynchronisation des variables du type et du corps d'un ↵herbelin
point-fixe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3504 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵herbelin
une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09Export M + Module M <: SIGcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la ↵desmettr
nouvelle organisation des reels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3424 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Add an example with Ring.bertot
Modified obj_magic.out because some formulas changed representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3403 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:58:05 +0000