aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.coq
Commit message (Collapse)AuthorAge
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
| | | | | | | | | | | | | | | | | | | | | | * le type ad des adresses est maintenant un alias vers le N de NArith, qui lui est isomorphe. * toutes les operations sur ces adresses (p.ex. un xor bit a bit) sont maintenant dans de nouveaux fichiers du repertoire NArith. * Intmap utilise maintenant le meme type option que le reste du monde * etc etc... Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs utilisant Intmap sont adaptees en consequence. Me demander si besoin ma moulinette d'adaptation (incomplete). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵Gravatar letouzey2006-03-28
| | | | | | OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un debut de proprietes pour les FSetWeakGravatar letouzey2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
| | | | | | | | | | | | | pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularisation des preuves concernant la logique classique, ↵Gravatar herbelin2006-03-05
| | | | | | l'indiscernabilité des preuves et l'axiome K git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zmax et ZminmaxGravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8033 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8020 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8015 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7586 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7529 85f007b7-540e-0410-9357-904b9bb8a0f7
* new congruenceGravatar corbinea2005-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7
* reflexive tautoGravatar corbinea2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7233 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6670 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6400 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6086 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5429 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5205 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et ↵Gravatar herbelin2003-11-29
| | | | | | states7; Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5028 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5023 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5003 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4977 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4969 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4953 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4915 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4890 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4887 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4885 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4827 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4817 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4811 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4776 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2003-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4742 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux fichiers dans LogicGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4729 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4704 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4682 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage en v8 de PolyList en List et List en MonoListGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵Gravatar herbelin2003-09-23
| | | | | | TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression DatatypesSyntax et PeanoSyntax qui était videsGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4386 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4229 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4207 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 01:14:31 +0000