aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2006-04-29suite de l'ajout des FSets/FMaps dans les theories standardsletouzey
-> OrderedTypeEx: des exemples de OrderedType -> OrderedTypeAlt: une definition alternative de OrderedType -> FSetAVL et FMapAVL: realisation a coup d'AVL -> FMapPositive: realisation a coup d'arbre binaire (selon les chiffres binaires de la cle) -> FMapIntMap : realisation en utilisant IntMap -> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine: on peut ne pas les compiler en passant l'option "-fsets no" a configure, de facon similaire a "-reals no" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-29meilleur nommage pour PairOrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-29qq proprietes de plus sur Ncompareletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8771 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Standardisation du nom des méthodes de Evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-272-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8744 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26suite du pont entre Bvector et Nletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8736 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25Un gros coup de lifting pour IntMap: letouzey
* 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
2006-04-25un lemme de double inclusionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-10New unification can solve the problem without eta-expansion, msozeau
but is bugguy with it. Temporary fix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8691 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8687 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06ouverture du bon scope (positive_scope) derriere le constructeur Npos de Nletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8685 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05on utilise explicitement Prop/iff pour certains morphismes pour eviter des ↵letouzey
warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-30Réajout de eq_rec_eq oublié lors de la modularisation de Eqdepherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8674 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29pour coqdocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28Nommage explicite de certains "intro" pour préserver la compatibilitéherbelin
en préparation du passage à des inductifs à polymorphisme de sorte ("sigT R" va devenir de type le type de R, càd Set) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵letouzey
OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17ajout d'un debut de proprietes pour les FSetWeakletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16deux tags $ mal formesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8640 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵letouzey
des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16utilisation de removeA dans FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8636 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15renommage NoRedun vers le plus joli NoDupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Typoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8634 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Typoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8633 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Ajout de fonctions sur les listesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8632 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Réparation de FSet (back to 8628)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15encore un essailetouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8630 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15reparation des $letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey
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
2006-03-05Modularisation des preuves concernant la logique classique, ↵herbelin
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
2006-03-05Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8135 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Renommage du IP classique pour éviter confusion avec IP constructifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8132 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Ajout étude IP généralisé, Gödel-Dummett, buveurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8131 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Petite simplification en passantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8122 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Titres moins envahissants pour coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8121 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-27quelques raccourcis commodes + un f_equal plus efficaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8100 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Ajout 'exists! x:A, P (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8086 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Ajout 'exists! x:A, Pherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22Minimum pour documentation TeX de la biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8082 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8078 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Bug Scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8034 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Nettoyage Bool:herbelin
Suppression de bool_2, bool_4 et bool_5 très ad hoc Renommage des lemmes demorgan* qui n'énoncent en fait pas les lois de de Morgan Tentative partielle de renommage (un peu) plus uniforme Pour les Hint: - bool_5 de core remplacé en mettant exact diff_false_true dans core (un peu plus faible mais marche dans la pratique pour les contribs) - bool_2 remplacé par la transitivité sur bool (plus fort mais OK dans la pratique, et pas trop fort pour ne pas atteindre la force de trans_eq) - bool_4 apparemment pas utilisé - andb_false_elim, spécifique, apparemment pas utilisé, et supprimé comme hint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8031 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Unification max_case et max_case2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8030 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Unification min_case et min_case2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8029 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-11Commentaires et compatibilité coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8026 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-10code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8022 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 20:02:23 +0000