aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2003-10-21ajoutsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4680 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-20R passe dans Set !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4677 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-1720 est uniquement associatif a gaucheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4672 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Des implicites plus 'naturels' pour eq_ind, identity_ind and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4669 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16nouvelle syntaxe de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16lettac -> setbarras
suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Syntax errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4653 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Suppression des surcharge de regles de grammaire en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4650 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Pour eviter des regles redondantes en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4647 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16FTC_P2 maintenant dans RIneqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4646 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Ajout de quelques lemmes clesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4645 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Affichage = au lieu de == en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4642 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Nettoyage argument de nilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4639 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Changement 'as notation' en 'where notation'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4632 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Argument de except, error implicite seulement en v8; Changement 'as ↵herbelin
notation' en 'where notation' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4628 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Argument de None implicite seulement en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4627 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Argument implicite pour None, error, exceptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4620 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Notations pour l'exponentiationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4618 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Enregistrement '^' en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4617 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11mise a jour nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10nat_scope ouvert par defautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4591 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4590 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10type_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4589 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Suppression de definitions equivalentesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4588 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Notation '^'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4586 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Plus d'Eval Computeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4584 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10MAJ commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4583 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Delimiters N devient 'nat'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4579 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-10Renommage en v8 de PolyList en List et List en MonoListherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4557 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01Retour sur la version non optimisee de 'add' pour compatibilite; renommage ↵herbelin
Un_suivi_de et Zero_suivi_de; nouveaux resultats sur 'times' et 'entier' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4511 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4507 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-28une induction de moins dans lt_eq_lt_decletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4495 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-28well_founded_induction de nouveau transparentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4494 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26'Open Local Scope' en attendant que le core_scope sache se mettre devant ↵herbelin
implicitement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4485 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Induction -> NewInduction; '++' pour appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4483 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Passage de Destruct a NewDestruct; '-' pour negbherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4480 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Structuration de fast_integer en operations sur positive, proprietes des ↵herbelin
operations sur positive, operations sur Z, proprietes des operations sur Z; suppression section; true_sub devient definition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4479 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-25add_x_x de fast_integer vers auxiliaryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4475 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-25Retour provisoire a une sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4474 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Suppression section, ce qui evite de repliquer les declarations d'Infixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4470 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Destruct/Induction -> NewDestruct/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4469 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Destruct -> NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4468 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4465 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4464 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4463 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵herbelin
TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 22:15:11 +0000