diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-11 08:34:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-11 08:34:20 +0000 |
| commit | 3768be5b5416c5c4ea159e5d8779f8393ada733a (patch) | |
| tree | 8f50b55a2d0f575e5673098f3aad5b09a3fa7548 | |
| parent | c1bc3bc1d4ef6e6f2ccab4ae0b58db124b39c41a (diff) | |
Ajout paramétricité du nom de la base de hint dans auto et trivial
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7835 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 313ff6321..8f537a601 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1013,6 +1013,13 @@ let interp_ident ist id = str ") should have been bound to an identifier") with Not_found -> id +let interp_hint_base ist s = + try match List.assoc (id_of_string s) ist.lfun with + | VIntroPattern (IntroIdentifier id) -> string_of_id id + | _ -> user_err_loc(loc,"", str "An ltac name (" ++ str s ++ + str ") should have been bound to a hint base name") + with Not_found -> s + let interp_intro_pattern_var ist id = try match List.assoc id ist.lfun with | VIntroPattern ipat -> ipat @@ -1720,8 +1727,10 @@ and interp_atomic ist gl = function HypLocation(interp_hyp ist gl id,hloc)) *) (* Automation tactics *) - | TacTrivial l -> Auto.h_trivial l - | TacAuto (n, l) -> Auto.h_auto (option_app (interp_int_or_var ist) n) l + | TacTrivial l -> Auto.h_trivial (option_app (List.map (interp_hint_base ist)) l) + | TacAuto (n, l) -> + Auto.h_auto (option_app (interp_int_or_var ist) n) + (option_app (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) | TacDestructConcl -> Dhyp.h_destructConcl |