diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 18:45:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 18:45:43 +0000 |
| commit | 7661293dc0b600ae45bc5b2a434db7043332d72d (patch) | |
| tree | 348ede9912080d858ea7c487264cdeccdf47f451 /parsing/g_tacticnew.ml4 | |
| parent | d2d14e4a2ebb16335e9c7d6a03bfe44e9db64d00 (diff) | |
Cablage en dur de inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tacticnew.ml4')
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index b17907844..b03aaf868 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -257,6 +257,10 @@ GEXTEND Gram [ [ "in"; idl = LIST1 hypident -> idl | -> [] ] ] ; + simple_clause: + [ [ "in"; idl = LIST1 id_or_meta -> idl + | -> [] ] ] + ; fixdecl: [ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot; ":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ] @@ -381,6 +385,27 @@ GEXTEND Gram TacSymmetry ido | IDENT "transitivity"; c = constr -> TacTransitivity c + (* Equality and inversion *) + | IDENT "dependent"; k = + [ IDENT "simple"; IDENT "inversion" -> SimpleInversion + | IDENT "inversion" -> FullInversion + | IDENT "inversion_clear" -> FullInversionClear ]; + hyp = quantified_hypothesis; + ids = with_names; co = OPT ["with"; c = constr -> c] -> + TacInversion (DepInversion (k,co,ids),hyp) + | IDENT "simple"; IDENT "inversion"; + hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp) + | IDENT "inversion"; + hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + TacInversion (NonDepInversion (FullInversion, cl, ids), hyp) + | IDENT "inversion_clear"; + hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp) + | IDENT "inversion"; hyp = quantified_hypothesis; + "using"; c = constr; cl = simple_clause -> + TacInversion (InversionUsing (c,cl), hyp) + (* Conversion *) | r = red_tactic; cl = clause -> TacReduce (r, cl) (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) |