aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-12-24Ajout delimiteur et arguments de scope pour listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5145 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24Bug affichage Decomposeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5144 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24MAJ Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5143 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24La correction precedente a mis en evidence un defaut de l'utilisation de ↵herbelin
intro_using qui ne garantit pas que le nom est vraiment celui demande; nouvelle correction (et suppression evbd inutile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5142 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5140 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23'of' restait par erreur mot-cle dans psyntax.ml4 en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Reparation semantique casse de Pose en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5138 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 ↵herbelin
dans induction/destruct qui marche maintenant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5137 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Retablissement de GIntuition juste pour FSetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5136 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Finalement, espacement autour du ':' pour a la fois exists, forall et funherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5135 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Affichage opaqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5133 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Bug commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5132 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Renommages des hypotheses transformees car en raison des possibles ↵herbelin
dependances, il n'y a pas de garantie de pouvoir les effacer pour garder le meme nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5131 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Changement numero magique; message d'erreur en cas de mauvaise syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5130 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5129 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-22Mise en valeur intropattern de paires et acceptation dans le 'as' de ↵herbelin
induction/inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5128 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5127 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5126 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5125 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-21Traduction PolyList/List dans la qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-20MAJ messages d'erreurs en accord avec la docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5123 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-20Bug rattrapage erreur locate_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5122 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5121 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5120 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5119 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Suppression de l'espace avant les notations commencant par un identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5118 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Inductive Types : seuls les petits types sont unitairesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5117 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Bug affichage des metas dans un environnement avec definitions locales (bug 277)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5116 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Substitution dans REvar; reparation bug 277herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5115 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application ↵herbelin
pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Reset Initial uniquement interactivementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5113 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19name_app accessible a tous dans Nameopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5111 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5110 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-17Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5109 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-17ajout test de non-regression Clear d'une def localebarras
reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5107 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16Correction bug 371 (sub_match retournait des instances non closes)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5106 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16MAJ suppression 250herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5105 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16coqide menus on golasmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5104 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16exists | --> exists ,barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5103 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5101 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5100 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoinherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5098 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15Protection du nom Eval pour eviter conflit avec Eval inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5097 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5096 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:19:26 +0000