diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-20 14:02:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-20 14:02:58 +0000 |
| commit | 98f6a9d847f4fac14696f51096c8334c9bffda6f (patch) | |
| tree | 3ab3dabe0f93f38b17434976f0b0c9833b8e3ff5 /tactics/hiddentac.ml | |
| parent | fbcd19a076f255614012fd076863ca296c1b2626 (diff) | |
Only one "in" clause in "destruct" even for a multiple "destruct".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 73aeec501..d642a38db 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -83,12 +83,12 @@ let h_simple_induction_destruct isrec h = let h_simple_induction = h_simple_induction_destruct true let h_simple_destruct = h_simple_induction_destruct false -let h_induction_destruct isrec ev l = - abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) -> - List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l)) - (induction_destruct ev isrec l) -let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl] -let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl] +let h_induction_destruct isrec ev (l,cl) = + abstract_tactic (TacInductionDestruct (isrec,ev,(List.map (fun (c,e,idl) -> + List.map inj_ia c,Option.map inj_open_wb e,idl) l,cl))) + (induction_destruct ev isrec (l,cl)) +let h_new_induction ev c e idl cl = h_induction_destruct ev true ([c,e,idl],cl) +let h_new_destruct ev c e idl cl = h_induction_destruct ev false ([c,e,idl],cl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) |