aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-03-13Mise en place temporaire d'un afficheur de 'language' pour le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5474 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-13Backtrack sur la réparation de Abstract qui casse autre chose; le problème ↵herbelin
en présence de variables de section est plus subtil et sa résolution est reportée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5473 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5472 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Bug inversion abstract_constr_expr et prod_constr_exprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5471 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12coq.spec n\'est plus parametrebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5470 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Retablissement de la correction bug d'inversion faite dans la version 1.116 ↵herbelin
et malencontreusement passe a la trappe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5469 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Ne pas ajouter le contexte de section dans Abstract, il est deja inclus ↵herbelin
(avec possibles modifications par clear) dans le contexte de but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5468 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12bug des points fixes (pb avec la contrib Matrices)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5467 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Correction d'un defaut dans la globalisation des variables de notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5466 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Bug compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5465 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12ajout decimal_exp pour interpreter les notations decimalesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5464 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Correctionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5462 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5461 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Test l'interprétation des scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5460 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout exemple Instherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5459 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout vieil exemple de coq-clubherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout d'un vieil exemple de N. Magaudherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5457 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ooops ! bug in firstorder fixed (let's hope no one noticed)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5456 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11code obsoleteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5455 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Suppression de la distinction entre elimination de Type vers Type ou pas ↵herbelin
(False, eq, Unit ont maintenant les bonnes proprietes pour fonctionner partout) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5454 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Branchement EmptyT, UnitT, IT vers leur equivalent dans Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5453 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout bug #540herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5452 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11reals: renamed type option into field_rel_optionmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5451 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 21:33:01 +0000