diff options
| author | jforest | 2006-03-21 21:54:43 +0000 |
|---|---|---|
| committer | jforest | 2006-03-21 21:54:43 +0000 |
| commit | dfa81d7860309029d100cd5348d2dd6bd8fa33c9 (patch) | |
| tree | 6421299af0b72711fff483052951dee4b0e53fa1 /tactics/tacinterp.ml | |
| parent | b8a287758030a451cf758f3b52ec607a8196fba1 (diff) | |
+ destruct now works as induction on multiple arguments :
destruct x y z using scheme
+ replace c1 with c2 <in hyp> has now a new optional argument <as tac>
replace c1 with c2 by tac tries to prove c2 = c1 with tac
+ I've also factorize the code correspoing to replace in extractactics
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 12c319b947..ee4e61179b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -677,7 +677,7 @@ let rec intern_atomic lf ist x = | TacSimpleDestruct h -> TacSimpleDestruct (intern_quantified_hypothesis ist h) | TacNewDestruct (c,cbo,ids) -> - TacNewDestruct (intern_induction_arg ist c, + TacNewDestruct (List.map (intern_induction_arg ist) c, option_app (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacDoubleInduction (h1,h2) -> @@ -1780,7 +1780,7 @@ and interp_atomic ist gl = function | TacSimpleDestruct h -> h_simple_destruct (interp_quantified_hypothesis ist h) | TacNewDestruct (c,cbo,ids) -> - h_new_destruct (interp_induction_arg ist gl c) + h_new_destruct (List.map (interp_induction_arg ist gl) c) (option_app (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist ids) | TacDoubleInduction (h1,h2) -> @@ -2037,7 +2037,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with option_app (subst_raw_with_bindings subst) cbo, ids) | TacSimpleDestruct h as x -> x | TacNewDestruct (c,cbo,ids) -> - TacNewDestruct (subst_induction_arg subst c, + TacNewDestruct (List.map (subst_induction_arg subst) c, (* Julien F. est-ce correct? *) option_app (subst_raw_with_bindings subst) cbo, ids) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) |