aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-04-02Added back the tactics [apply -> ident], etc. to Tactics.v afteremakarov
committing the extension of the general sequence operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9743 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Extension to the general sequence operator (tactical). Now in addition to ↵emakarov
the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0. The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Intégration de la modification suggérée par Michal Moskal (cf msg sur Coq ↵notin
Club du 31/03/2007) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9741 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Réparation de NArith/BinPos.v suite au commit #9739notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9740 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-01Removed the definition of extensions of apply to equivalencesemakarov
(apply -> H, etc.), which prevented Coq compilation. These tactics require an extension of syntax: t1; [t2 | .. ], which has to be submitted first. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9739 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-30Added the following theorems to BinPos:emakarov
Pplus_xO Pmult_Sn_m Pcompare_eq_Lt (a generalization of Pcompare_Gt_Lt) Pcompare_eq_Gt (a generalization of Pcompare_Lt_Gt) Pcompare_refl_id (a generalization of Pcompare_refl) Pcompare_Lt_eq_Lt (a generalization of Pcompare_Lt_Lt) Pcompare_Gt_eq_Gt (a generalization of Pcompare_Gt_Gt) Pcompare_p_Sp Pcompare_p_Sq (one of the defining axioms of < ) Pcompare_1 (1 is the least positive number) Added the following theorems to BinNat: Nrect (defined in terms of new Prect) Nrect_base Nrect_step (the analogout statement in BinPos is called Prect_succ) Nrec_base Nrec_step Nmult_Sn_m Nsucc_0 Ncompare_0 (0 is the least natural number) Ncompare_n_Sm (one of the defining axioms of < ) Also, defined Nind and Nrec in terms of Nrect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9738 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-30Added new tactics for applying equivalences (iff) to Tactics.v:emakarov
"apply -> t", "apply <- t", "apply -> t in H" and "apply <- t in H" . Also added the tactic false_hyp based on absurd_hyp. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9737 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-30Modifications dans Makefile: notin
make et make world déclenchent maintenant la compilation des dépendances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9736 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-30Changement mineur du comportement de 'rewrite .. in * |-': si lenotin
constr avec lequel on réécrit contient une hypothèse H, on ne réécrit pas dans H (corrige le bug #1446) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9735 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-28Support for implicit formal argument types in Program ; parse types in type ↵msozeau
scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9734 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-27Modification de la vm:notin
- le type val_kind n'embarque plus le constr (pb de cohérence avec le context); - en revanche, lors du calcul d'une valeur, on calcule aussi l'ensemble des variables nommées dont la valeur peut dépendre; - lors du clear_hyps, si la valeur dépend d'une variable effacée, on invalide le calcul. Corrige le bug #1419 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9733 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-26Make multiple patterns work again with Program while simplifying the code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9732 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-26stupid me: ?f two times in a patternletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9731 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-26PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ↵letouzey
OrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9730 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-22Correction des bugs #1455 et #1456notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9728 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-22Remove debugging code committed by accidentlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9727 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-22A tentative fix for bug #1455lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9726 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-21Suppression des sauts de lignes superflus de Show Script ↵notin
(test-suite/output/Tactics.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9725 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-20Correction bug affichage des notations des noms de fonctions appliquéesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9723 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-20Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still ↵msozeau
a bit broken git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9722 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-20ajout contrib/dp/Dp.vofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9721 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-20traces Ergofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9720 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Forgot to update to new castmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9719 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an ↵msozeau
obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Un chouia de portabilité en plus et pas de test si pas de bogomipsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9714 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-17MAJ test complexité pour considérer le cas d'un temps avec un nombreherbelin
arbitraire de décimales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9713 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-16Correction du bug #1441notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9712 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest
correction bug 1442 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9710 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Test de non-régression pour commit 9673herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9709 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Typosherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9708 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Prévention notations récursives sans terminal à gauche et qui font bouclerherbelin
le parser git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9706 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Add destruct_call variant where naming of introduced hypotheses is possible. ↵msozeau
Destruct_exists destructs pairs now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9705 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-14Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ↵msozeau
bug introduced by previous commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9704 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-14Bug dans Makefile (COQINSTALLPREFIX)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9702 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-14Removed an unnecessary argument (p : positive) in Prect_base.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9701 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-13Solve obligation handling bug of trying to solve automatically at Next ↵msozeau
Obligation time. Now done at Qed or Defined. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9700 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-13Correction bug #1439 (comportement de replace by)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9699 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-12Proof simplification for eq_nat_dec et le_lt_dec: induction over letouzey
2nd arg m can simply be a destruct. This helps (vm_)compute __a lot__. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9698 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-11correction du bug 1432jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9696 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-11Remove bugguy notationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9695 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-09bug#1434 importing fonctor arguments, now it works.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9693 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-08Create a program_scope in subtac Utilsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9692 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-08Add Program keywords to coqwcmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9691 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-08Transparence de eq_dec et lt_dec daans OrderedTypeFactsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-07Application suggestion #1430 de Yevgeniy pour TEXINPUTSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9687 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-06màj dépendances .v: SubtacTactics.volmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9686 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-28FSetInterface: new item choose_equal in the spec S (request of P. Casteran)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9684 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-28The right tactics for definitions using measures.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9683 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-27Fix wf bug from F. Besson and work on ineqs generation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9682 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 22:36:27 +0000