aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Collapse)AuthorAge
* 'Open Local Scope' en attendant que le core_scope sache se mettre devant ↵Gravatar herbelin2003-09-26
| | | | | | implicitement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Structuration de fast_integer en operations sur positive, proprietes des ↵Gravatar herbelin2003-09-26
| | | | | | 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
* add_x_x de fast_integer vers auxiliaryGravatar herbelin2003-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour provisoire a une sectionGravatar herbelin2003-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression section, ce qui evite de repliquer les declarations d'InfixGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Destruct -> NewDestructGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de lemmes de IntMap vers ZArithGravatar herbelin2003-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de la politique de V8only: V8only tout seul signifieGravatar herbelin2003-09-21
| | | | | | | | | 'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conflit de nom Pplus dans positive et dans polynomial (de ring)Gravatar herbelin2003-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵Gravatar herbelin2003-09-21
| | | | | | aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Section et report Infix hors sectionGravatar herbelin2003-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵Gravatar herbelin2003-09-19
| | | | | | 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
* Bind et Delimit pour positive et Z (hors section)Gravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4368 85f007b7-540e-0410-9357-904b9bb8a0f7
* principes de récurrences plus efficaces pour l'extractionGravatar letouzey2003-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4309 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zdiv plus efficace: r+r -> 2*rGravatar letouzey2003-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zabs_ZsgnGravatar letouzey2003-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un peu d'aide pour le traducteurGravatar herbelin2003-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq.Init.Logic.eq au lieu de eqGravatar filliatr2003-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4239 85f007b7-540e-0410-9357-904b9bb8a0f7
* recursion bien fondee sur des pairsGravatar filliatr2003-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments superflus pour Zlength_nilGravatar herbelin2003-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4162 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite changements ZArith en vu de librairie FSetGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4149 85f007b7-540e-0410-9357-904b9bb8a0f7
* quelques adaptations de Zarith en vu de la nouvelle librarie FSetGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement d'un lemme sur nat de ZArith vers ArithGravatar herbelin2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4146 85f007b7-540e-0410-9357-904b9bb8a0f7
* Import nat_scopeGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4132 85f007b7-540e-0410-9357-904b9bb8a0f7
* niveau 49 devient nextGravatar herbelin2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4089 85f007b7-540e-0410-9357-904b9bb8a0f7
* Concentration des notations officielles dans Init/Notations; restructuration ↵Gravatar herbelin2003-05-21
| | | | | | de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: toolbar/autosaveGravatar monate2003-05-07
| | | | | | | Hugo: Suppression du type dans les notations == et <> entre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Open ScopeGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'associativité gauche au niveau 3 en vieille syntaxe !Gravatar herbelin2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3803 85f007b7-540e-0410-9357-904b9bb8a0f7
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans une tactique toplevelGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug precedenceGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation à la nouvelle sémantique plus uniforme de "Match term"Gravatar herbelin2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3567 85f007b7-540e-0410-9357-904b9bb8a0f7
* bit vectorsGravatar filliatr2003-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-installation nombres dans les motifs sur ZGravatar herbelin2002-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3483 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilite times1 (suite)Gravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle preuve de times_convert pour nouvelle définition de timesGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité times1Gravatar herbelin2002-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un axiome en attendant la mise a jour de la preuve de times_convertGravatar herbelin2002-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration sensible de l'efficacité de la multiplicationGravatar herbelin2002-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Z_scope doit annuler l'affichage de = entreGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction affichage entiers en cas d'échecGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement affichage des entiers de natGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3279 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 03:35:49 +0000