diff options
| author | letouzey | 2012-10-06 10:08:45 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:45 +0000 |
| commit | e1bdb515ee2f701bfc56f1bcf4a8e404f759a38a (patch) | |
| tree | 52eb681313f840b3d46d633ed0440e3ad96ace9a /tactics/elim.ml | |
| parent | f975575187d0a19e7cc1afc43459a92eeb12b3f1 (diff) | |
remove Refiner.abstract_tactic and similar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index a25a370922..685a70badb 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -122,14 +122,11 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls -let h_decompose l c = - Refiner.abstract_tactic (decompose_these c l) +let h_decompose l c = decompose_these c l -let h_decompose_or c = - Refiner.abstract_tactic (decompose_or c) +let h_decompose_or = decompose_or -let h_decompose_and c = - Refiner.abstract_tactic (decompose_and c) +let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) @@ -174,7 +171,6 @@ let double_ind h1 h2 gls = (introElimAssumsThen (induction_trailer abs_i abs_j)) ([],[]) (mkVar id)))) gls -let h_double_induction h1 h2 = - Refiner.abstract_tactic (double_ind h1 h2) +let h_double_induction = double_ind |