aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-12-18Suppression de l'affichage des instances des ?nherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1144 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1143 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1142 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1141 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Debut de nettoyage de Simplmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1140 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1139 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1138 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1137 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Redondant or incompatible instantiations in clenv_assign now correctly trappedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1136 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1135 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Suppression du warning several default clausesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1134 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1133 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Le bon choix, c'est finalement identifier = stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1132 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1131 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Mise en place d'un module Ident avec test de l'efficacité quand ↵herbelin
identifier=string git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1130 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bug env vis à vis du let inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1129 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15pb niveaumayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1128 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15suppression warning et calcule type dans replace_by_meta dans tous les casfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1127 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1126 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15 - suppression mind_extract_paramsfilliatr
- contraintes univers parametres inductifs prises en compte - exception UniverseInconsistency donne un message "Error: Universe Inconsistency" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1125 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1124 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Réparation de bugs de LoadPathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1123 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées ↵herbelin
'Set Implicit Arguments' and co git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1122 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Petite réorganisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1121 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bug des locaux au premier niveau des modules qui disparaissaient de ↵herbelin
l'environnement (changement de is_section_p) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1120 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bugs calcul du prédicat des Cases et Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1119 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1118 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Printermohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1117 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15test univers, inductifs et sectionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1116 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1115 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bug sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1114 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Mauvais env donné à new_isevarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1112 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Oubli test de correction à l'instantiation des evarsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1111 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1109 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Amélioration message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1108 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Évaluation forcée des objets mis dans les streamsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1107 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Amélioration message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1106 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1105 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14LetIn dans Simplmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1104 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bug sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1103 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Enfin trouvé la cause d'exception; suppression de la capsule de rattrapageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1102 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14MAJ commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1101 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1100 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Fichier de test pour les Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1099 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Autorisation de parenthèses autour des constructeurs dans le filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1098 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Raffinement erreur Wrong Predicateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1097 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases ↵herbelin
devient systématiquement dépendent; blindage de certaines erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1096 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bug dans les alias de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1095 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 12:48:52 +0000