aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2001-11-03interversion de deux Elim dans In_dec pour que la fonction extraite soit ↵letouzey
efficace git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2156 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27Simplification de deux preuves. En outre ca simplifie leur extraction.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2082 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27and_rec redondantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Deplacement des setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18modif test constmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1977 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-12Rustine pour gérer inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1954 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Un look un peu plus avenant aux productions des règles de grammaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1953 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Du bon usage des commentaires coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1952 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Conformité des commentaires au format coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1951 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-30Fin de la modif Exc/optionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13Rétablissement nom de section Map après résolution bugs surcharge de nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1898 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13Protection des commentaires pour coqtex et coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1897 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-19modifs de preuves (plus simples)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1858 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16modif Map sectionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1851 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout du .v pour la tactique Setoid_replaceclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1842 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Oubli Save + je sais plusmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1792 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Ajouts de lemmes (pour Float)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1791 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1790 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-04Correction bug outsidemayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1778 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-31Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant ↵herbelin
les thms interessants en hints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1775 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Correction d'un bug du pretty-printclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1770 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Modification pour passage p-automatesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-07ex d'utilisation de fourier avec fieldmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1735 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25coqwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1711 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24correction nommayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1702 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Ajout de Rseries et Rtrigo_funmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1686 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24(Again) Little corrections for Library doccoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1684 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Ajout Realsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1676 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Ajouts Realsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1675 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23(One more) Minor layout adjustments for Library doccoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1674 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Minor layout adjustments for Library doccoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1672 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout tactics Realsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1658 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Library doc adjustments (until page 140)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19typofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1636 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de fonctions proposees par Cuiht Alvaradomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1630 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19BoolEq.v, une egalite generique a valeur dans boolmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1628 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1622 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1618 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Remplacement Euclid_def Euclid_proof par Euclidmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1617 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Changement syntax pour Rinvmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1611 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-06 13:05:33 +0000