aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* *** empty log message ***Gravatar desmettr2001-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2280 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2279 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration nommage hypothèses NewInduction (et incompatibilités)Gravatar herbelin2001-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2274 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2273 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2272 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2270 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2269 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2268 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2267 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traitement t de -1<>0Gravatar delahaye2001-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur le commit du 30.11.2001Gravatar delahaye2001-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2263 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2262 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2260 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2259 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du fichierGravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de Reals pour integrer les modificationsGravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2255 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du fichier concernant le carre et la racine carreeGravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2254 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration de nouveaux lemmesGravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2253 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration de nouveaux lemmes.Gravatar desmettr2001-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2251 85f007b7-540e-0410-9357-904b9bb8a0f7
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2232 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un fichier Max dans Arith, et enrichissement du Min.Gravatar letouzey2001-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des fonctions tail-recursives tail_plus et tail_mult.Gravatar letouzey2001-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'Export redondantsGravatar herbelin2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2190 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression d'axiomes dans Rstar, Newman et IntegersGravatar letouzey2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2187 85f007b7-540e-0410-9357-904b9bb8a0f7
* interversion de deux Elim dans In_dec pour que la fonction extraite soit ↵Gravatar letouzey2001-11-03
| | | | | | efficace git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de Logic_Type.sigT, redondant avec Specif.sigTGravatar herbelin2001-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRGravatar delahaye2001-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification de deux preuves. En outre ca simplifie leur extraction.Gravatar letouzey2001-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2082 85f007b7-540e-0410-9357-904b9bb8a0f7
* and_rec redondantGravatar letouzey2001-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des setoides.Gravatar clrenard2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif test constGravatar mayero2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rustine pour gérer inject_natGravatar herbelin2001-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un look un peu plus avenant aux productions des règles de grammaireGravatar herbelin2001-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1953 85f007b7-540e-0410-9357-904b9bb8a0f7
* Du bon usage des commentaires coqwebGravatar herbelin2001-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conformité des commentaires au format coqwebGravatar herbelin2001-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fin de la modif Exc/optionGravatar mohring2001-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout option , Exc --> option, et lemmes dans les theoriesGravatar mohring2001-08-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement nom de section Map après résolution bugs surcharge de nomsGravatar herbelin2001-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection des commentaires pour coqtex et coqwebGravatar herbelin2001-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
* modifs de preuves (plus simples)Gravatar mayero2001-07-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1858 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif Map sectionGravatar mohring2001-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du .v pour la tactique Setoid_replaceGravatar clrenard2001-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli Save + je sais plusGravatar mayero2001-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajouts de lemmes (pour Float)Gravatar mayero2001-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1791 85f007b7-540e-0410-9357-904b9bb8a0f7