aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵herbelin
noms d'hypothèses; Changement de natural en int_or_var pour 'do' et 'fail' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5420 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵herbelin
noms d'hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5419 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Changement de natural en int_or_var pour 'do' et 'fail' pour ↵herbelin
paramétrisation dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Simplification preuveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5417 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Tactic Notation et with-namesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5416 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵herbelin
variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Correction oubli du cas pas d'arguments implicites du toutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5413 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 22:35:16 +0000