diff options
| author | herbelin | 2007-09-30 19:06:41 +0000 |
|---|---|---|
| committer | herbelin | 2007-09-30 19:06:41 +0000 |
| commit | 40a581ecfcec8d8dbb5d21f331464dc2b34cadff (patch) | |
| tree | fd448dc1caa2846ad028eb77fd3b5b17feedde81 | |
| parent | ef5551e4ca73a93c0820f03ac702ee96e5e7b431 (diff) | |
Suite de 10157
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10157 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 15b6f7abdd..1a6c18e4dd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -695,7 +695,9 @@ let rec intern_atomic lf ist x = | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) - | TacDAuto (n,p) -> TacDAuto (option_map (intern_or_var ist) n,p) + | TacDAuto (n,p,lems) -> + TacDAuto (option_map (intern_or_var ist) n,p, + List.map (intern_constr ist) lems) (* Derived basic tactics *) | TacSimpleInduction h -> @@ -2121,7 +2123,9 @@ and interp_atomic ist gl = function | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) | TacDestructConcl -> Dhyp.h_destructConcl | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 - | TacDAuto (n,p) -> Auto.h_dauto (option_map (interp_int_or_var ist) n,p) + | TacDAuto (n,p,lems) -> + Auto.h_dauto (option_map (interp_int_or_var ist) n,p) + (pf_interp_constr_list ist gl lems) (* Derived basic tactics *) | TacSimpleInduction h -> @@ -2435,7 +2439,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDestructHyp (b,id) -> TacDestructHyp(b,id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) - | TacDAuto (n,p) -> TacDAuto (n,p) + | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems) (* Derived basic tactics *) | TacSimpleInduction h as x -> x |