diff options
| author |  Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
| commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
| tree | dabcac548e299fee1da464c93b3dba98484f45b1 /tactics/elim.ml | |
| parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) | |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
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 *) |