aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-03-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5450 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5449 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5448 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-10Ajout tactiques stepl et stepr de Nimègueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5447 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-10Correction bug internalisation 'context'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5446 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5445 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-09bug de l'inversion (coq-bugs #529)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5444 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-09option -l de coqc non reconnue (coq-bugs #509)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5443 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-09bug affichage des cofixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5442 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5441 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-08correction de bugs des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5439 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-06the output the parser should produce nowbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5438 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-06changed the test for obj_magic.v to be less sensitive to changesbertot
nobody was paying attention anyway git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5437 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5436 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur ↵herbelin
la copie traduisante de pr_id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5434 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5433 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5432 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-04Reparation ROmega V8/Omega ZERO/POS/NEGmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5431 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-04ROmegamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5430 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5429 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03adaptation V8 version Pierre Cregutmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5428 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03ide: silent behavior better, save icon, -byte worksmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5427 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03takes better account of the new possibility to pass a parametric count argumentbertot
to both 'do' and 'fail' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5425 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03removes capital letters in two tactic names.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5424 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03make sure the implicit argument indications are in the right orderbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5423 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5422 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5421 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:21:06 +0000