aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2007-04-05Mise en place d'une nouvelle strategie plus efficace pour les preuves de ↵jforest
Function. => Changement d'ordre et de forme des obligations de preuve generees (pas de la semantique des obligations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9746 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-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-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-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-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-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-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-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-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-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-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-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
2007-02-24Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Opacity parameterization for obligations working.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9675 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-23Debug wellfounded defs, work on cleaning obls envsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9674 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-22Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish ↵notin
#1375) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9672 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-19Correct coq depend, add eq_rect elimination tactic to SubtacTacticsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9661 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-19Various little subtac fixes, add some useful tactics.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9659 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16lift params appropriately, do not need to coerce to tyconmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9653 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Update implementation for dependent types. Works just as well as before for ↵msozeau
simple cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9651 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-14encodage des typesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9646 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-14tactique yicesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9645 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-12Bug mineur dans la generation des principes d'induction pour Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9643 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-12Fix matching on dependent types, taking a safe stand.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9641 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-11Correction d'un bug dans la génération des principes d'inductionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9639 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-09Retour r9310 en attendant mieuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9629 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-09Separate Tactics in subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9627 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-08Add lif then else for if in bool.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9626 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-08Fix myinjection tactic, generalize coercion for applicationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9625 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Fix mistake naming my Tactics file Tactics :)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9624 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Add tactics for induction on subterms.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9623 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Meilleur anglais (cf 9619)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Various subtac fixes. Add inequalities in pattern matching branches when ↵msozeau
needed, handle undo for the default tactic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9608 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07doc de ring/field + option infinite -> completenessbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9602 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-05changement dans ring specification du sign, divisionbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9591 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-03Work on ineqs generation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9590 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterherbelin
de cacher l'instance de la règle figurant dans g_constr (report révision 9588 de 8.1 vers trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9589 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02field: introduction de Get_goalbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9587 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02ring: introduction de Get_goalbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9586 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02Now 1/x * x simplifies to 1thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9585 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Abbreviation of order notation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9576 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-30constr_of_pat bug with nested patterns.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9556 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-30 17:11:49 +0000