Préservation compatibilité interprétation quantified hypothesis (provisoire ?) + export nouvelle macro pour maple.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8975 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 13 insertions, 5 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e3a8c7cac..e34a165d8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1345,7 +1345,9 @@ let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
-      with Not_found -> NamedHyp id
+      with Not_found 
+      | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*)
+   -> NamedHyp id
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
@@ -1911,6 +1913,10 @@ and interp_atomic ist gl = function
     try tactic_of_value v gl 
     with NotTactic -> user_err_loc (loc,"",str "not a tactic")
 
+let make_empty_glob_sign () =
+  { ltacvars = ([],[]); ltacrecvars = []; 
+    gsigma = Evd.empty; genv = Global.env() }
+
 (* Initial call for interpretation *)
 let interp_tac_gen lfun debug t gl = 
   interp_tactic { lfun=lfun; debug=debug } 
@@ -1922,6 +1928,10 @@ let eval_tactic t = interp_tactic { lfun=[]; debug=get_debug() } t
 
 let interp t = interp_tac_gen [] (get_debug()) t
 
+let eval_ltac_constr gl t =
+  interp_ltac_constr { lfun=[]; debug=get_debug() } gl
+    (intern_tactic (make_empty_glob_sign ()) t )
+
 (* Hides interpretation for pretty-print *)
 let hide_interp t ot gl =
   let ist = { ltacvars = ([],[]); ltacrecvars = []; 
@@ -2285,10 +2295,6 @@ let make_absolute_name (loc,id) =
       str "There is already an Ltac named " ++ pr_id id);
   kn
 
-let make_empty_glob_sign () =
-  { ltacvars = ([],[]); ltacrecvars = []; 
-    gsigma = Evd.empty; genv = Global.env() }
-
 let add_tacdef isrec tacl =
 (*  let isrec = if !Options.p1 then isrec else true in*)
   let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 057f20be5..bccdd3943 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -121,6 +121,8 @@ val eval_tactic : glob_tactic_expr -> tactic
 
 val interp : raw_tactic_expr -> tactic
 
+val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr
+
 val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
 
 (* Hides interpretation for pretty-print *)