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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index c6453f076..4435d57ab 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -60,12 +60,24 @@ type 'a induction_arg = | ElimOnAnonHyp of int type intro_pattern_expr = - | IntroOrAndPattern of intro_pattern_expr list list + | IntroOrAndPattern of case_intro_pattern_expr | IntroWildcard | IntroIdentifier of identifier +and case_intro_pattern_expr = intro_pattern_expr list list + type 'id clause_pattern = int list option * ('id * int list) list +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + +type ('c,'id) inversion_strength = + | NonDepInversion of inversion_kind * 'id list * case_intro_pattern_expr + | DepInversion of inversion_kind * 'c option * case_intro_pattern_expr + | InversionUsing of 'c * 'id list + type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b type pattern_expr = constr_expr @@ -111,10 +123,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis | TacNewInduction of 'constr induction_arg * 'constr with_bindings option - * intro_pattern_expr list list + * case_intro_pattern_expr | TacSimpleDestruct of quantified_hypothesis | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option - * intro_pattern_expr list list + * case_intro_pattern_expr | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr @@ -155,6 +167,9 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacSymmetry of 'id option | TacTransitivity of 'constr + (* Equality and inversion *) + | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis + (* For ML extensions *) | TacExtend of loc * string * ('constr,'tac) generic_argument list |