aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
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
2003-06-13Require Exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4152 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13FSets, mais pas compile' par make worldfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13suite changements ZArith en vu de librairie FSetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4149 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13quelques adaptations de Zarith en vu de la nouvelle librarie FSetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4148 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-06-12INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le ↵herbelin
traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4140 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Import nat_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4132 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Suppression d'une occurrence superflue d'argument de type dans Notation ↵herbelin
sachant que les 2 occurrences ne sont pas forcement dans le meme scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4131 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Deplacement delimiteur T dans Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4130 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Bug niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4092 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29niveau 49 devient nextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4091 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:46:25 +0000