From 0a770151ee4dabe240d2fa08dc58f98f334eb9d1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 20 Jan 2003 00:25:46 +0000
Subject: Petits bugs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3540 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index aa1f37a839..2550bfb5af 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -79,7 +79,7 @@ type value =
   | VRec of value ref
 
 (* Signature for interpretation: val_interp and interpretation functions *)
-and interp_sign =
+type interp_sign =
   { lfun : (identifier * value) list;
     lmatch : (int * constr) list;
     debug : debug_info }
@@ -834,6 +834,11 @@ let get_debug () = !debug
 let eval_ident ist id =
   try match List.assoc id ist.lfun with
   | VIdentifier id -> id
+  | VConstr c as v when isVar c ->
+      (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *)
+      (* c is then expected not to belong to the proof context *)
+      (* would be checkable if env were known from eval_ident *)
+      destVar c
   | _ -> user_err_loc(loc,"eval_ident",str "should be bound to an identifier")
   with Not_found -> id
 
@@ -1569,7 +1574,7 @@ let interp_tacarg sign ast = (*unvarg*) (val_interp sign ast)
 let tac_interp lfun lmatch debug t = 
   tactic_interp { lfun=lfun; lmatch=lmatch; debug=debug } t
 
-let interp = tac_interp [] [] (get_debug())
+let interp = fun t -> tac_interp [] [] (get_debug()) t (* Side-effect *)
 
 (* Hides interpretation for pretty-print *)
 let hide_interp t ot gl =
-- 
cgit v1.2.3