aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-12-25Alias variable_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Effet réorganisation Classopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1202 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; ↵herbelin
réorganisation; bugs discharge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1201 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug vieux Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1200 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1199 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Traducteur automatique de scripts vernacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1198 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22*** empty log message ***mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1197 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1196 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1195 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22cleanallherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1194 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Insertion COQPATHPREFIX pour isntallation localeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1193 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Oublisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1192 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22MAJ V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1191 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Mauvais numéro de version de camlp4 requisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1190 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Pour créer les archives distribuéesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1189 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Novembre -> Décembreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1188 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Création...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1187 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1186 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Traduction en francais de 'CHANGES' dont le contenu était en françaisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1185 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Re-MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1184 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1183 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Bug d'affichage à cause des << ... >>herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1182 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Qualification des inductifs dans Print indherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1181 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1180 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1179 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Toujours Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1178 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20espacementsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1177 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug prédicat old Case/Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1176 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Suppression warning variable de filtrage en majusculeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1175 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1174 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1173 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Test pour empêcher 2 sections de même nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Oublié de supprimer du code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1171 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug mauvais environnement dans le test d'eta-conversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1170 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ↵herbelin
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
2000-12-20Toujours Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1168 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20ajout ident_or_constrarg pour NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1167 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Induction/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1166 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug dans l'utilisation de l'option debugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1165 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert ↵herbelin
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
2000-12-20Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints ↵herbelin
qui fait l'instantiation des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1163 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Ajout set_lcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1162 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Scripts de correction d'uriherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1161 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1160 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Non verbose par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1159 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Correction pour les variables abstraites dans les Tactic Definitionsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1158 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19DEMOS passe et MUTUAL-EXCLUSION aussi modulo Realizerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1157 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19correction de bugs sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1156 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Découpage des différentes fonctionnalités de build_mutual et ↵herbelin
definition_structure + export des sous-fonctions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1155 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Export fonction testant si un inductive est un recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1154 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 03:50:32 +0000