aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵herbelin
VERNAC EXTEND (e.g. Hint Rewrite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5525 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17install de coqdocbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5523 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17suppression du ./ devant (et .\ sous Windows)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5522 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5521 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Parsing des V8Notation avec motif recursif en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5520 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Definition de la notation de la paire par un motif recursifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5519 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Definition de la notation de la paire par un motif recursifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5518 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Utilisation de '..' pour la notation concrete des motifs recursifs de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5517 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Motifs recursifs de notations: prise en compte de l'associativite et des ↵herbelin
notations de pattern de filtrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5516 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Amelioration affichage des notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5515 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17CREDITSmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5514 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5513 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5512 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5511 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications ↵herbelin
au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5509 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16Mise a jour ZArith/Cregutmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5508 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16mise a jour des menusmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5507 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16Adaptation a la v7 du message d'erreur Match_failureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5506 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16typocoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5505 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16application patch de Lionel Elie Mamane pour option -R et chemins ↵filliatr
relatifs/absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5504 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16install de pcoq incorrect + spec rpmbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5503 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16pages de man pour coqwc et coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5502 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16page de man pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5501 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16page de man pour coqwcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5500 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5499 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5498 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation pour release (suite)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5497 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15bug d'Inversion #529 (pb avec ordre d'evaluation)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5496 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5495 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Ajout affichage contexte localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5494 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15ajout des Print Scopes dans liste commandes sans effetmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5493 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation packages V8.0-cdrombarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5492 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Ajout d'un fichier COPYRIGHTmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5491 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Mise a jour CREDITS en vue copyrightmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5490 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation packages V8.0-cdrombarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5489 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation packages V8.0-cdrombarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5488 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Nouvelle reparation pour Abstract en presence de variables de contexte: on ↵herbelin
considere une var de but comme var de contexte si elle a meme nom, meme type, et, le cas echeant meme corps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5487 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15To make that the translation process does not fail on data produced bybertot
the logical engine (rather than the parser), where Some Anonymous appears instead of None in the patterns of xlate_return_info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5486 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15oopscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5485 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15mise a jour depend.coq7 vs ROmegamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5484 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15identification ./f et f dans coqdep -sortfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5483 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Parametersfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5482 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5481 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14minor changescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5480 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14congruence now handles disequalitiescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5479 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fix (2e)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5478 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5477 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de choix de noms courts avec Suresnes/BDDbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5476 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-13Nouvel exemple; correction du contexte du précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5475 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:06:34 +0000