aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-01-09Meta Definition -> Tactic Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1238 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Tactic Definition -> Meta Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1237 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1236 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-04Rajout de la restriction de l'instance en cas d'unification de 2 variables ↵herbelin
existentielles (heuristique qui existait en V6) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1235 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-03Prise en compte des ??herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1234 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-03Let doit etre utilise dans le mode de preuvedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1233 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1232 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-27Améliorationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1230 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-27Bug installation non localeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1228 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1227 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Dernière MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1226 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1225 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Bug de contextesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1224 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1223 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Elimination des coupuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1222 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour ↵herbelin
accélérer la réduction dans Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1221 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26On n'évite plus les globaux dans Intro, mais on les évite dans Abstractherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1220 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce ↵herbelin
dernier qui échouera si c'est pas normalisé de tête git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1218 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1217 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Command -> Constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1216 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1215 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Normalisation betaiota du pattern avant enregistrement comme hint (certains ↵herbelin
développements exploite cette caractéristique) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1214 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25bug head_pattern_boundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1213 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Modifs sur le langage de tactiques et pas de "ë" dans Micaeladelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1212 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1211 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug confusion existS/sigSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1210 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Token n'est plus un keywordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1209 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Command -> Constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1208 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1207 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Remplacement de debug en assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1206 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug discharge process_classherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1205 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25find_section_variable : un traducteur id -> sp pour variables de section; ↵herbelin
variable_strength change de type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1204 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 09:00:39 +0000