aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/fast_integer.v
AgeCommit message (Collapse)Author
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-14Quelques oublis pour que les notations marchent bienherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4907 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Oubli report Nul/Posherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4895 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Oubli BinNatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4826 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4818 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵herbelin
de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4721 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report ↵herbelin
'relation' pour compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4720 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4702 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Type relation dans Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4691 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-10Plus d'Eval Computeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4584 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-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-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-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-22Deplacement de lemmes de IntMap vers ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4440 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Section et report Infix hors sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4421 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵herbelin
meme si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4417 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Bind et Delimit pour positive et Z (hors section)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4368 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Deplacement de le_minus de fast_integer vers Minusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4162 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-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 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-12-10Compatibilite times1 (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3415 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Nouvelle preuve de times_convert pour nouvelle définition de timesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3396 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-07Compatibilité times1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3387 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-06Un axiome en attendant la mise a jour de la preuve de times_convertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3386 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-06Amélioration sensible de l'efficacité de la multiplicationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3384 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-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-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:35:04 +0000