From 3768be5b5416c5c4ea159e5d8779f8393ada733a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 08:34:20 +0000
Subject: 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
---
 tactics/tacinterp.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 313ff63210..8f537a601f 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
-- 
cgit v1.2.3