aboutsummaryrefslogtreecommitdiff
path: root/theories/Arith/Mult.v
AgeCommit message (Collapse)Author
2009-11-02Remove various useless {struct} annotationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-15Tentative de relecture des scripts de Mult.v au regard des tactiques actuellesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11224 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28- Modification de la déf de minus et pred conformément aux remarques deherbelin
Assia et Benjamin W. de telle sorte qu'ils respectent le critère de décroissance structurelle lorsqu'utilisés dans un point-fixe. - Ajout des noms "standard" des lemmes de Peano et correction d'un nom de BinInt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30Changement esthétique de la preuve de mult_is_onenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10274 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et ↵notin
plus_is_one) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10273 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13Ajout du théorème mult_minus_distr_lnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9237 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Nouveaux lemmes 'canoniques'; compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4901 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Independance vis a vis noms variables liees; partie sur bool dans Zboolherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4876 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Redondancesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4806 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4701 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-06-13Deplacement d'un lemme sur nat de ZArith vers Arithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4146 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4013 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4010 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3923 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Implicit Variables Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-15Ajout des fonctions tail-recursives tail_plus et tail_mult.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2194 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08ajout des lemmes Zimmermanmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10mise sous CVS du repertoire theories/Arithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 17:12:35 +0000