diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9a2682fd..ff53bfe8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -3189,12 +3189,19 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = end let induction_destruct isrec with_evars = function - | [],_ -> tclIDTAC - | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl) - | (a,b,c)::l,cl -> + | [],_,_ -> tclIDTAC + | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl) + | (a,b)::l,None,cl -> tclTHEN - (induct_destruct isrec with_evars (a,b,c,cl)) - (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l) + (induct_destruct isrec with_evars ([a],None,b,cl)) + (tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l) + | l,Some el,cl -> + let check_basic_using = function + | a,(None,None) -> a + | _ -> error "Unsupported syntax for \"using\"." + in + let l' = List.map check_basic_using l in + induct_destruct isrec with_evars (l', Some el, (None,None), cl) let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls) let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) @@ -3406,7 +3413,7 @@ let intros_symmetry = (* Transitivity tactics *) -(* This tactic first tries to apply a constant named trans_eq, where eq +(* This tactic first tries to apply a constant named eq_trans, where eq is the name of the equality predicate. If this constant is not defined and the conclusion is a=b, it solves the goal doing Cut x1=x2; |