diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 2e079567..889ead5e 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: elim.ml 7538 2005-11-08 17:14:52Z herbelin $ *) +(* $Id: elim.ml 9842 2007-05-20 17:44:23Z herbelin $ *) open Pp open Util @@ -136,14 +136,16 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls +let inj_open c = (Evd.empty,c) + let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) + Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l) let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) + Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c) let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) + Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c) (* The tactic Double performs a double induction *) |