diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-21 13:07:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-21 13:07:30 +0000 |
| commit | 04ceaad7583afcd85754b909ae25e7128646ff54 (patch) | |
| tree | b45b773df0b73bf4e057b62c2b722e894a700745 /tactics/tacinterp.ml | |
| parent | b6fead62658797f75be03d1a952b771f4c260c0f (diff) | |
NewDestruct/NewInduction acceptent l'option "using"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 71ec78b4c..afc77834d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -503,9 +503,13 @@ let rec glob_atomic lf ist = function (* Derived basic tactics *) | TacOldInduction h -> TacOldInduction (glob_quantified_hypothesis ist h) - | TacNewInduction c -> TacNewInduction (glob_induction_arg ist c) + | TacNewInduction (c,cbo) -> + TacNewInduction (glob_induction_arg ist c, + option_app (glob_constr_with_bindings ist) cbo) | TacOldDestruct h -> TacOldDestruct (glob_quantified_hypothesis ist h) - | TacNewDestruct c -> TacNewDestruct (glob_induction_arg ist c) + | TacNewDestruct (c,cbo) -> + TacNewDestruct (glob_induction_arg ist c, + option_app (glob_constr_with_bindings ist) cbo) | TacDoubleInduction (h1,h2) -> let h1 = glob_quantified_hypothesis ist h1 in let h2 = glob_quantified_hypothesis ist h2 in @@ -1634,9 +1638,13 @@ and interp_atomic ist = function (* Derived basic tactics *) | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist h) - | TacNewInduction c -> h_new_induction (interp_induction_arg ist c) + | TacNewInduction (c,cbo) -> + h_new_induction (interp_induction_arg ist c) + (option_app (interp_constr_with_bindings ist) cbo) | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist h) - | TacNewDestruct c -> h_new_destruct (interp_induction_arg ist c) + | TacNewDestruct (c,cbo) -> + h_new_destruct (interp_induction_arg ist c) + (option_app (interp_constr_with_bindings ist) cbo) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in |