aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2003-09-22Implicits maintenant au courant pour l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4441 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-21Changement de la politique de V8only: V8only tout seul signifieherbelin
'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
2003-09-21Conflit de nom Pplus dans positive et dans polynomial (de ring)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4429 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵herbelin
aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4428 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵herbelin
aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4427 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4426 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19'::' est deja pris en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4423 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-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le ↵herbelin
traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4420 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Ajout notation :: pour consherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4418 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-12Suppression DatatypesSyntax et PeanoSyntax qui était videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4383 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout et MAJ commandes de scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4375 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Bind et Delimit pour Rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4373 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Bind et Delimit pour natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4370 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-09-12Bind et Delimit pour Rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4367 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4353 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05principes de récurrences plus efficaces pour l'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4309 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Zdiv plus efficace: r+r -> 2*rletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4308 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Zabs_Zsgnletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4307 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-01Passage de 'relation' à Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4288 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Affichage {}+{}, niveau paire au plus hautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4250 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Un peu d'aide pour le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4249 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-18Coq.Init.Logic.eq au lieu de eqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4239 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-08recursion bien fondee sur des pairsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4224 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-24suppression de FSets (redevient une contrib)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4205 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-24docfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4204 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-24concat; debut splitfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4203 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23joinfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4199 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23add_tree : sur type tree plutot que sur type tfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4198 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23merge_bis et debug joinfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4197 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20removfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4191 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20mergefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4190 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20remove_min, remove_maxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4189 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19addfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4183 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19bal: preuve termineefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4182 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19bal: premier cas hl > hr + 2filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4181 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19typofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4179 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-18AVL: suitefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4177 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-18Arguments superflus pour Zlength_nilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4176 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-17AVL: suitefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4174 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-17AVL de caml: un debutfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4173 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16Ground depthfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4170 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16reparation fsets suite a changement de Groundfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4168 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-14Deplacement de le_minus de fast_integer vers Minusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13changement de spécif du foldletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4159 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13fcts tail-recursivesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4153 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-29 18:20:48 +0000