aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Bug confusion existS/sigSGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Token n'est plus un keywordGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1209 85f007b7-540e-0410-9357-904b9bb8a0f7
* Command -> ConstrGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1208 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de debug en assertGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug discharge process_classGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1205 85f007b7-540e-0410-9357-904b9bb8a0f7
* find_section_variable : un traducteur id -> sp pour variables de section; ↵Gravatar herbelin2000-12-25
| | | | | | variable_strength change de type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Alias variable_pathGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Effet réorganisation ClassopsGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1202 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un nom long pour les variables de section qui font classe ou coercion; ↵Gravatar herbelin2000-12-25
| | | | | | réorganisation; bugs discharge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug vieux MatchGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1200 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug prédicatGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traducteur automatique de scripts vernacGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1198 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mayero2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1197 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1196 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1195 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleanallGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Insertion COQPATHPREFIX pour isntallation localeGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1193 85f007b7-540e-0410-9357-904b9bb8a0f7
* OublisGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1192 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V7Gravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1191 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvais numéro de version de camlp4 requisGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour créer les archives distribuéesGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1189 85f007b7-540e-0410-9357-904b9bb8a0f7
* Novembre -> DécembreGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création...Gravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1187 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction en francais de 'CHANGES' dont le contenu était en françaisGravatar herbelin2000-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-MAJGravatar herbelin2000-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1184 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug d'affichage à cause des << ... >>Gravatar herbelin2000-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1182 85f007b7-540e-0410-9357-904b9bb8a0f7
* Qualification des inductifs dans Print indGravatar herbelin2000-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1181 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1180 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1179 85f007b7-540e-0410-9357-904b9bb8a0f7
* Toujours InductionGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1178 85f007b7-540e-0410-9357-904b9bb8a0f7
* espacementsGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug prédicat old Case/MatchGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression warning variable de filtrage en majusculeGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1174 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test pour empêcher 2 sections de même nomsGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oublié de supprimer du code mortGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug mauvais environnement dans le test d'eta-conversionGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1170 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ↵Gravatar herbelin2000-12-20
| | | | | | inductif où la constante la plus proche du Fix est prise en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Toujours InductionGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1168 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout ident_or_constrarg pour NewInductionGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Induction/NewInductionGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans l'utilisation de l'option debugGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Import module force l'ouverture du module même s'il était déjà ouvert ↵Gravatar herbelin2000-12-20
| | | | | | afin de pouvoir re-rendre visible des noms ayant été cachés depuis l'ouverture du module; renommage de open_module en import_module avec cette nouvelle spéc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints ↵Gravatar herbelin2000-12-20
| | | | | | qui fait l'instantiation des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout set_lcGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Scripts de correction d'uriGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1161 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-17 23:55:28 +0000