aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-03-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5412 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5411 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5410 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Correction sur commit précédent : Tactics.cut réduisait de manière ↵herbelin
inappropriée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5409 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Ajout 'replace in'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5408 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Ajout IntroPattern comme type d'argument génériqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5407 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Déplacement définition intro_pattern_expr dans Genargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5406 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵herbelin
des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Déplacement définition intro_pattern_expr dans Genargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5404 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Protection d'un 'clear' qui peut etre dependantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5403 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01ocaml 3.07 -> 3.06filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5402 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5401 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5400 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Exemple de Fredericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Expansion du type par nécessité dans le cas d'affichage d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5398 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28MAJ Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5397 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Traduction 'Cases' en pattern-matchingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5396 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Eviter la stricte redondance de regles de grammaires v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5395 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 00:03:13 +0000