aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2003-11-12Ajout lemmes; independance vis a vis noms variables liees; restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4873 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout partie sur bool anciennement dans Zmischerbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4872 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemmes; independance vis a vis noms variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12On sait jamaisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4862 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4845 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Oubli BinNatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4826 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans impredicativiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4822 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Des oublisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4818 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4816 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres ↵herbelin
positifs et naturels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4809 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Preuve de l'incoherence de {A}+{~A} avec Set impredicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4808 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Redondancesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4806 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵herbelin
de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4780 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Renforcement significatif du resultat principalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Rien de bien importantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4777 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4774 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02AC + EXT -> EMherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4772 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Relations entre le choix (forme relationnelle) avec restriction ou nonherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4771 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Renommage bool en boolP pour eviter la qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Restauration preference Rge a Rle pour compatibilite...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4769 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Restauration preference Rge a Rle pour compatibilite...; petit nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4768 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x'; suppression notations - et / unaire en V7 pour compatibilite V7.4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4750 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-29Choix sous sa forme relationnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4741 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ordre (symbolique) des Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4738 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Passage de la notations de paire dans core_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4737 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Passage des notations de type dans type_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4736 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout %core; MAJ niveau connecteurs logiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4732 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4725 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4724 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4723 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28La logique sur Type inclut celle sur Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4721 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report ↵herbelin
'relation' pour compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4720 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Bug du commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4716 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4709 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4702 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4701 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Redondance de dec_eq_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4692 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Type relation dans Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4691 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Maintenant avant Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4681 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 12:37:58 +0000