Restructuration interpréteur de tactique: plus d'évaluation partielle à la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif

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

6 files changed, 599 insertions, 685 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cda51446e3..ef92ff3bc2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -131,12 +131,19 @@ let set_var_scope loc id (_,_,scopes) (_,_,varscopes) =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let intern_var (env,impls,scopes) (vars1,vars2,_) loc id =
-  (* Is [id] bound in  *)
+let intern_var (env,impls,scopes) ((vars1,unbndltacvars),vars2,_) loc id =
+  (* Is [id] bound in current env or ltac vars bound to constr *)
   if Idset.mem id env or List.mem id vars1
   then
     RVar (loc,id), (try List.assoc id impls with Not_found -> []), []
   else
+  (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
+  try
+    match List.assoc id unbndltacvars with
+      | None -> user_err_loc (loc,"intern_var",
+	  pr_id id ++ str " ist not bound to a term")
+      | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+  with Not_found ->
   (* Is [id] a section variable *)
   let _ = Sign.lookup_named id vars2 in
   (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
@@ -327,8 +334,8 @@ let check_capture loc ty = function
   | _ ->
       ()
 
-let locate_if_isevar loc id = function
-  | RHole _ -> RHole (loc, AbstractionType id)
+let locate_if_isevar loc na = function
+  | RHole _ -> RHole (loc, AbstractionType na))
   | x -> x
 
 (**********************************************************************)
@@ -471,7 +478,8 @@ let internalise isarity sigma env allow_soapp lvar c =
 	if nal <> [] then check_capture loc1 ty na;
 	let ids' = name_fold Idset.add na ids in
 	let body = iterate_prod loc2 (ids',impls,scopes) ty body nal in
-	RProd (join_loc loc1 loc2, na, intern true env ty, body)
+	let ty = locate_if_isevar loc1 na (intern true env ty) in
+	RProd (join_loc loc1 loc2, na, ty, body)
     | [] -> intern true env body
 
   and iterate_lam loc2 isarity (ids,impls,scopes as env) ty body = function
@@ -540,18 +548,18 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Idset.empty
 
-let interp_rawconstr_gen isarity sigma env impls allow_soapp lvar c =
+let interp_rawconstr_gen isarity sigma env impls allow_soapp ltacvar c =
   internalise isarity sigma (extract_ids env, impls, [])
-    allow_soapp (lvar,Environ.named_context env, []) c
+    allow_soapp (ltacvar,Environ.named_context env, []) c
 
 let interp_rawconstr sigma env c =
-  interp_rawconstr_gen false sigma env [] false [] c
+  interp_rawconstr_gen false sigma env [] false ([],[]) c
 
 let interp_rawtype sigma env c =
-  interp_rawconstr_gen true sigma env [] false [] c
+  interp_rawconstr_gen true sigma env [] false ([],[]) c
 
 let interp_rawtype_with_implicits sigma env impls c =
-  interp_rawconstr_gen true sigma env impls false [] c
+  interp_rawconstr_gen true sigma env impls false ([],[]) c
 
 (*
 (* The same as interp_rawconstr but with a list of variables which must not be
@@ -593,20 +601,28 @@ let retype_list sigma env lst =
 
 (*  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
 
+type ltac_sign = 
+  identifier list * (identifier * identifier option) list
+
+type ltac_env = 
+  (identifier * Term.constr) list * (identifier * identifier option) list
+
 (* Interprets a constr according to two lists *)
 (* of instantiations (variables and metas)    *)
 (* Note: typ is retyped *)
-let interp_constr_gen sigma env lvar lmeta c exptyp =
-  let c = interp_rawconstr_gen false sigma env [] false (List.map fst lvar) c
+let interp_constr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
+  let c = interp_rawconstr_gen false sigma env [] false 
+    (List.map fst ltacvar,unbndltacvar) c
   and rtype lst = retype_list sigma env lst in
-  understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;;
+  understand_gen sigma env (rtype ltacvar) (rtype lmeta) exptyp c;;
 
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
-let interp_openconstr_gen sigma env lvar lmeta c exptyp =
-  let c = interp_rawconstr_gen false sigma env [] false (List.map fst lvar) c
+let interp_openconstr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
+  let c = interp_rawconstr_gen false sigma env [] false
+    (List.map fst ltacvar,unbndltacvar) c
   and rtype lst = retype_list sigma env lst in
-  understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;;
+  understand_gen_tcc sigma env (rtype ltacvar) (rtype lmeta) exptyp c;;
 
 let interp_casted_constr sigma env c typ = 
   understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
@@ -658,20 +674,21 @@ let pattern_of_rawconstr lvar c =
   let p = pat_of_raw metas [] lvar c in
   (!metas,p)
 
-let interp_constrpattern_gen sigma env lvar c =
-  let c = interp_rawconstr_gen false sigma env [] true (List.map fst lvar) c in
-  let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
+let interp_constrpattern_gen sigma env (ltacvar,unbndltacvar) c =
+  let c = interp_rawconstr_gen false sigma env [] true
+    (List.map fst ltacvar,unbndltacvar) c in
+  let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) ltacvar in
   pattern_of_rawconstr nlvar c
 
 let interp_constrpattern sigma env c =
-  interp_constrpattern_gen sigma env [] c
+  interp_constrpattern_gen sigma env ([],[]) c
 
 let interp_aconstr vars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) vars in
   let c = for_grammar (internalise false Evd.empty (extract_ids env, [], [])
-    false ([],Environ.named_context env,vl)) a in
+    false (([],[]),Environ.named_context env,vl)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4c185a788e..5478957b56 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -34,10 +34,16 @@ open Topconstr
 
 type implicits_env = (identifier * Impargs.implicits_list) list
 
+type ltac_sign = 
+  identifier list * (identifier * identifier option) list
+
+type ltac_env = 
+  (identifier * constr) list * (identifier * identifier option) list
+
 (* Interprets global names, including syntactic defs and section variables *)
 val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
 val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> 
-    bool -> identifier list -> constr_expr -> rawconstr
+    bool -> ltac_sign -> constr_expr -> rawconstr
 
 (*s Composing the translation with typing *)
 val interp_constr        : evar_map -> env -> constr_expr -> constr
@@ -62,25 +68,24 @@ val type_judgment_of_rawconstr :
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it*)
 val interp_constr_gen     :
-  evar_map -> env -> (identifier * constr) list ->
-    (int * constr) list -> constr_expr -> constr option -> constr
+  evar_map -> env -> ltac_env -> (int * constr) list -> constr_expr -> 
+    constr option -> constr
 
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it, and turning unresolved evar into metas*)
 val interp_openconstr_gen     :
-  evar_map -> env -> (identifier * constr) list ->
+  evar_map -> env -> ltac_env ->
     (int * constr) list -> constr_expr -> constr option -> evar_map * constr
 
 (* Interprets constr patterns according to a list of instantiations
   (variables)*)
 val interp_constrpattern_gen :
-  evar_map -> env -> (identifier * constr) list -> constr_expr ->
-    int list * constr_pattern
+  evar_map -> env -> ltac_env -> constr_expr -> int list * constr_pattern
 
 val interp_constrpattern : 
   evar_map -> env -> constr_expr -> int list * constr_pattern
 
-val interp_reference : identifier list -> reference -> rawconstr
+val interp_reference : ltac_sign -> reference -> rawconstr
 
 (* Interprets into a abbreviatable constr *)
 val interp_aconstr : identifier list -> constr_expr -> interpretation
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 43162f05d4..68d1425aa0 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -16,7 +16,7 @@ open Printer
 
 (* Debug information *)
 type debug_info =
-  | DebugOn
+  | DebugOn of int
   | DebugOff
   | Exit
 
@@ -31,20 +31,37 @@ let db_pr_goal = function
 let help () =
   msgnl (str "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit")
 
+(* Prints raised exceptions *)
+let rec db_print_error = function
+  | Type_errors.TypeError(ctx,te) -> 
+      hov 0 (str "Type error:" ++ spc ())
+  | Pretype_errors.PretypeError(ctx,te) ->
+      hov 0 (str "Pretype error:" ++ spc ())
+  | Logic.RefinerError e -> 
+      hov 0 (str "Refiner error:" ++ spc ())
+  | Stdpp.Exc_located (loc,exc) ->
+      db_print_error exc
+  | Util.UserError(s,pps) -> 
+      hov 1 (str"Error: " ++ pps)
+  | GlobalizationError q ->
+      hov 0 (str "Error: " ++ Libnames.pr_qualid q ++ str " not found") ++ 
+  | _ ->
+      hov 0 (str "Uncaught exception ")
+
 (* Prints the state and waits for an instruction *)
-let debug_prompt goalopt tac_ast =
+let debug_prompt level goalopt tac_ast f exit =
   db_pr_goal goalopt;
   msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++ fnl ());
 (*         str "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
 (*  mSG (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl () ++ fnl () ++
          str "----<Enter>=Continue----s=Skip----x=Exit----");*)
   let rec prompt () =
-    msg (fnl () ++ str "TcDebug > ");
+    msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
     let inst = read_line () in
 (*    mSGNL (mt ());*)
     match inst with
-    | ""  -> DebugOn
+    | ""  -> DebugOn (level+1)
     | "s" -> DebugOff
     | "x" -> Exit
     | "h" ->
@@ -53,20 +70,27 @@ let debug_prompt goalopt tac_ast =
         prompt ()
       end
     | _   -> prompt () in
-  prompt ()
+  match prompt () with
+    | Exit -> exit ()
+    | d ->
+	try f d
+	with e when Logic.catchable_exception e ->
+	  ppnl (str "Level " ++ int level ++ str ": " ++ db_print_error e); 
+	  raise e
 
 (* Prints a constr *)
 let db_constr debug env c =
-  if debug = DebugOn then
+  if debug <> DebugOff & debug <> Exit then
     msgnl (str "Evaluated term --> " ++ prterm_env env c)
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) =
-  if debug = DebugOn then
+  if debug <> DebugOff & debug <> Exit then
     msgnl (str "Matched hypothesis --> " ++ str (Names.string_of_id id^": ") ++
            prterm_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if debug = DebugOn then
+  if debug <> DebugOff & debug <> Exit then
     msgnl (str "Matched goal --> " ++ prterm_env env c)
+
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index b05a33fdfc..1bb8a7f42d 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -18,12 +18,13 @@ open Term
 
 (* Debug information *)
 type debug_info =
-  | DebugOn
+  | DebugOn of int
   | DebugOff
   | Exit
 
 (* Prints the state and waits *)
-val debug_prompt : goal sigma option -> Tacexpr.raw_tactic_expr -> debug_info
+val debug_prompt : int -> goal sigma option -> Tacexpr.raw_tactic_expr ->
+      (debug_info -> 'a) -> (unit -> 'a) -> 'a
 
 (* Prints a constr *)
 val db_constr : debug_info -> Environ.env -> constr -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 64bf9371fd..5319b4fc08 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -42,10 +42,12 @@ open Hiddentac
 open Genarg
 open Decl_kinds
 
+(*
 let err_msg_tactic_not_found macro_loc macro =
   user_err_loc
     (macro_loc,"macro_expand",
      (str "Tactic macro " ++ str macro ++ spc () ++ str "not found"))
+*)
 
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
@@ -56,39 +58,40 @@ let skip_metaid = function
   | AI x -> x
   | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
 
+type ltac_type =
+  | LtacFun of ltac_type
+  | LtacBasic
+  | LtacTactic
+
 (* Values for interpretation *)
 type value =
-  | VClosure of interp_sign * raw_tactic_expr
   | VTactic of tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
-  | VFTactic of value list * (value list->tactic)
-  | VRTactic of (goal list sigma * validation)
-  | VContext of interp_sign * direction_flag
-      * (pattern_expr,raw_tactic_expr) match_rule list
+  | VRTactic of (goal list sigma * validation) (* For Match results *)
+                                               (* Not a true value *)
   | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
   | VVoid
   | VInteger of int
-  | VIdentifier of identifier (* idents which are not refs, as in "Intro H" *)
-  | VConstr of constr
+  | VIdentifier of identifier (* idents which are not bound, as in "Intro H" *)
+                              (* but which may be bound later, as in "tac" in*)
+                              (* "Intro H; tac" *)
+  | VConstr of constr         (* includes idents known bound and references *)
   | VConstr_context of constr
   | VRec of value ref
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 and interp_sign =
-  { evc : Evd.evar_map;
-    env : Environ.env;
-    lfun : (identifier * value) list;
+  { lfun : (identifier * value) list;
     lmatch : (int * constr) list;
-    goalopt : goal sigma option;
     debug : debug_info }
 
+let check_is_value = function
+  | VRTactic _ -> (* These are goals produced by Match *)
+   error "Immediate Match producing tactics not allowed in local definitions"
+  | _ -> ()
+
 (* For tactic_of_value *)
 exception NotTactic
 
-(* Gives the constr corresponding to a Constr tactic_arg *)
-let constr_of_VConstr = function
-  | VConstr c -> c
-  | _ -> anomalylabstrm "constr_of_VConstr" (str "Not a Constr tactic_arg")
-
 (* Gives the constr corresponding to a Constr_context tactic_arg *)
 let constr_of_VConstr_context = function
   | VConstr_context c -> c
@@ -115,25 +118,14 @@ let pr_value env = function
   | VIdentifier id -> pr_id id
   | VConstr c -> Printer.prterm_env env c
   | VConstr_context c -> Printer.prterm_env env c
-  | (VClosure _ | VTactic _ | VFTactic _ | VRTactic _ |
-     VContext _ | VFun _ | VRec _) -> str "<fun>"
+  | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>"
 
 (* Transforms a named_context into a (string * constr) list *)
 let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
 
-(* Transforms an id into a constr if possible *)
-let constr_of_id ist id =
-  match ist.goalopt with
-  | None -> construct_reference (Some (Environ.named_context ist.env)) id
-  | Some goal ->
-    let hyps = pf_hyps goal in
-    if mem_named_context id hyps then
-      mkVar id
-    else
-      let csr = global_qualified_reference (make_short_qualid id) in
-      (match kind_of_term csr with
-      | Var _ -> raise Not_found
-      | _ -> csr)
+(* Transforms an id into a constr if possible, or fails *)
+let constr_of_id env id = 
+  construct_reference (Some (Environ.named_context env)) id
 
 (* To embed several objects in Coqast.t *)
 let ((tactic_in : (interp_sign -> raw_tactic_expr) -> Dyn.t),
@@ -203,20 +195,20 @@ let look_for_interp = Hashtbl.find interp_tab
 
 (* Globalizes the identifier *)
 
-let find_reference ist qid =
+let find_reference env qid =
   (* We first look for a variable of the current proof *)
-  match repr_qualid qid, ist.goalopt with
-    | (d,id),Some gl when repr_dirpath d = [] & List.mem id (pf_ids_of_hyps gl)
+  match repr_qualid qid with
+    | (d,id) when repr_dirpath d = [] & List.mem id (ids_of_context env)
 	-> VarRef id
     | _ -> Nametab.locate qid
 
-let coerce_to_reference ist = function
+let coerce_to_reference env = function
   | VConstr c ->
       (try reference_of_constr c
       with Not_found -> invalid_arg_loc (loc, "Not a reference"))
 (*  | VIdentifier id -> VarRef id*)
   | v -> errorlabstrm "coerce_to_reference"
-      (str "The value" ++ spc () ++ pr_value ist.env v ++ 
+      (str "The value" ++ spc () ++ pr_value env v ++ 
        str "cannot be coerced to a reference")
 
 (* turns a value into an evaluable reference *)
@@ -266,7 +258,7 @@ let _ =
 
 (* Interpretation of extra generic arguments *)
 type genarg_interp_type =
-    interp_sign -> raw_generic_argument -> closed_generic_argument
+   interp_sign -> goal sigma -> raw_generic_argument -> closed_generic_argument
 let extragenargtab = ref (Gmap.empty : (string,genarg_interp_type) Gmap.t)
 let add_genarg_interp id f = extragenargtab := Gmap.add id f !extragenargtab
 let lookup_genarg_interp id = 
@@ -283,19 +275,31 @@ let unrec = function
 
 (* We have identifier <| global_reference <| constr *)
 
+let find_ident id (lfun,_,_,env) = 
+  List.mem id lfun or 
+  List.mem id (ids_of_named_context (Environ.named_context env))
+
 (* Globalize a name which can be fresh *)
-let glob_ident l ist x =
+let glob_ident l ist id =
   (* We use identifier both for variables and new names; thus nothing to do *)
-  if List.mem x (fst ist) then () else l:=x::!l;
-  x
+  if find_ident id ist then () else l:=id::!l;
+  id
 
 let glob_name l ist = function
   | Anonymous -> Anonymous
   | Name id -> Name (glob_ident l ist id)
 
+let get_current_context () =
+    try Pfedit.get_current_goal_context ()
+    with e when Logic.catchable_exception e -> 
+      (Evd.empty, Global.env())
+
+let weak = ref true
+
 (* Globalize a name which must be bound -- actually just check it is bound *)
-let glob_hyp (lfun,_) (loc,id) =
-  if List.mem id lfun then id
+let glob_hyp ist (loc,id) =
+  let (_,env) = get_current_context () in
+  if !weak or find_ident id ist then id
   else
 (*
     try let _ = lookup (make_short_qualid id) in id
@@ -309,8 +313,8 @@ let error_unbound_metanum loc n =
   user_err_loc
     (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound")
 
-let glob_metanum ist loc n =
-  if List.mem n (snd ist) then n else error_unbound_metanum loc n
+let glob_metanum (_,lmeta,_,_) loc n =
+  if List.mem n lmeta then n else error_unbound_metanum loc n
 
 let glob_hyp_or_metanum ist = function
   | AN id -> AN (glob_hyp ist (loc,id))
@@ -321,7 +325,7 @@ let glob_qualid_or_metanum ist = function
   | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n)
 
 let glob_reference ist = function
-  | Ident (loc,id) as r when List.mem id (fst ist) -> r
+  | Ident (loc,id) as r when find_ident id ist -> r
   | r -> Qualid (loc,qualid_of_sp (sp_of_global None (Nametab.global r)))
 
 let glob_ltac_qualid ist ref =
@@ -330,7 +334,7 @@ let glob_ltac_qualid ist ref =
   with Not_found -> glob_reference ist ref
 
 let glob_ltac_reference ist = function
-  | Ident (_loc,id) when List.mem id (fst ist) -> Ident (loc,id)
+  | Ident (_loc,id) when !weak or find_ident id ist -> Ident (loc,id)
   | r -> glob_ltac_qualid ist r
 
 let rec glob_intro_pattern lf ist = function
@@ -346,10 +350,10 @@ let glob_quantified_hypothesis ist x =
      statically check the existence of a quantified hyp); thus nothing to do *)
   x
 
-let glob_constr ist c =
+let glob_constr (lfun,_,sigma,env) c =
   let _ =
-    Constrintern.interp_rawconstr_gen false
-      Evd.empty (Global.env()) [] false (fst ist) c
+    Constrintern.for_grammar (Constrintern.interp_rawconstr_gen false
+      sigma env [] false (lfun,[])) c
   in c
 
 (* Globalize bindings *)
@@ -412,11 +416,11 @@ let glob_hyp_location ist = function
 let glob_pattern evc env lfun = function
   | Subterm (ido,pc) ->
       let lfun = List.map (fun id -> (id, mkVar id)) lfun in
-      let (metas,_) = interp_constrpattern_gen evc env lfun pc  in
+      let (metas,_) = interp_constrpattern_gen evc env (lfun,[]) pc  in
       metas, Subterm (ido,pc)
   | Term pc ->
       let lfun = List.map (fun id -> (id, mkVar id)) lfun in
-      let (metas,_) = interp_constrpattern_gen evc env lfun pc  in
+      let (metas,_) = interp_constrpattern_gen evc env (lfun,[]) pc  in
       metas, Term pc
 
 let glob_constr_may_eval ist = function
@@ -463,7 +467,7 @@ let extract_let_names lrc =
     lrc []
 
 (* Globalizes tactics *)
-let rec glob_atomic lf ist = function
+let rec glob_atomic lf (_,_,_,_ as ist) = function
   (* Basic tactics *)
   | TacIntroPattern l -> TacIntroPattern (List.map (glob_intro_pattern lf ist) l)
   | TacIntrosUntil hyp -> TacIntrosUntil (glob_quantified_hypothesis ist hyp)
@@ -558,26 +562,26 @@ let rec glob_atomic lf ist = function
   | TacExtend (_loc,opn,l) ->
       let _ = lookup_tactic opn in
       TacExtend (loc,opn,List.map (glob_genarg ist) l)
-  | TacAlias (_,l,body) -> failwith "TacAlias globalisation: TODO"
+  | TacAlias (_,l,body) as t ->
+      (* failwith "TacAlias globalisation: TODO" *)
+      t
 
 and glob_tactic ist tac = snd (glob_tactic_seq ist tac)
 
-and glob_tactic_seq (lfun,lmeta as ist) = function
+and glob_tactic_seq (lfun,lmeta,sigma,env as ist) = function
   | TacAtom (_loc,t) ->
       let lf = ref lfun in
       let t = glob_atomic lf ist t in
       !lf, TacAtom (loc, t)
   | TacFun tacfun -> lfun, TacFun (glob_tactic_fun ist tacfun)
-  | TacFunRec (name,tacfun) ->
-      lfun, TacFunRec (name,glob_tactic_fun ((snd name)::lfun,lmeta) tacfun)
   | TacLetRecIn (lrc,u) ->
       let names = extract_names lrc in
-      let ist = (names@lfun,lmeta) in
+      let ist = (names@lfun,lmeta,sigma,env) in
       let lrc = List.map (fun (n,b) -> (n,glob_tactic_fun ist b)) lrc in
       lfun, TacLetRecIn (lrc,glob_tactic ist u)
   | TacLetIn (l,u) ->
       let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist) c,glob_tacarg ist b)) l in
-      let ist' = ((extract_let_names l)@lfun,lmeta) in
+      let ist' = ((extract_let_names l)@lfun,lmeta,sigma,env) in
       lfun, TacLetIn (l,glob_tactic ist' u)
   | TacLetCut l ->
       let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg ist t) in
@@ -592,12 +596,12 @@ and glob_tactic_seq (lfun,lmeta as ist) = function
   | TacAbstract (tac,s) -> lfun, TacAbstract (glob_tactic ist tac,s)
   | TacThen (t1,t2) ->
       let lfun', t1 = glob_tactic_seq ist t1 in
-      let lfun'', t2 = glob_tactic_seq (lfun',lmeta) t2 in
+      let lfun'', t2 = glob_tactic_seq (lfun',lmeta,sigma,env) t2 in
       lfun'', TacThen (t1,t2)
   | TacThens (t,tl) ->
       let lfun', t = glob_tactic_seq ist t in
       (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun', TacThens (t, List.map (glob_tactic (lfun',lmeta)) tl)
+      lfun', TacThens (t, List.map (glob_tactic (lfun',lmeta,sigma,env)) tl)
   | TacDo (n,tac) -> lfun, TacDo (n,glob_tactic ist tac)
   | TacTry tac -> lfun, TacTry (glob_tactic ist tac)
   | TacInfo tac -> lfun, TacInfo (glob_tactic ist tac)
@@ -608,9 +612,9 @@ and glob_tactic_seq (lfun,lmeta as ist) = function
   | TacSolve l -> lfun, TacSolve (List.map (glob_tactic ist) l)
   | TacArg a -> lfun, TacArg (glob_tacarg ist a)
 
-and glob_tactic_fun (lfun,lmeta) (var,body) = 
+and glob_tactic_fun (lfun,lmeta,sigma,env) (var,body) = 
   let lfun' = List.rev_append (filter_some var) lfun in
-  (var,glob_tactic (lfun',lmeta) body)
+  (var,glob_tactic (lfun',lmeta,sigma,env) body)
 
 and glob_tacarg ist = function
   | TacVoid -> TacVoid
@@ -629,15 +633,15 @@ and glob_tacarg ist = function
                  str "Unknown dynamic: <" ++ str s ++ str ">"))
 
 (* Reads the rules of a Match Context or a Match *)
-and glob_match_rule (lfun,lmeta as ist) = function
+and glob_match_rule (lfun,lmeta,sigma,env as ist) = function
   | (All tc)::tl ->
       (All (glob_tactic ist tc))::(glob_match_rule ist tl)
   | (Pat (rl,mp,tc))::tl ->
-      let env = Global.env() in
       let lfun',metas1,hyps = glob_match_context_hyps Evd.empty env lfun rl in
       let metas2,pat = glob_pattern Evd.empty env lfun mp in
       let metas = list_uniquize (metas1@metas2@lmeta) in
-      (Pat (hyps,pat,glob_tactic (lfun',metas) tc))::(glob_match_rule ist tl)
+      (Pat (hyps,pat,glob_tactic (lfun',metas,sigma,env) tc))
+      ::(glob_match_rule ist tl)
   | [] -> []
 
 and glob_genarg ist x =
@@ -744,15 +748,10 @@ let is_match_catchable = function
   | e -> Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
-let rec verify_metas_coherence ist lcm = function
+let rec verify_metas_coherence gl lcm = function
   | (num,csr)::tl ->
-    if (List.for_all
-         (fun (a,b) ->
-            if a=num then
-              Reductionops.is_conv ist.env ist.evc b csr
-            else
-              true) lcm) then
-      (num,csr)::(verify_metas_coherence ist lcm tl)
+    if (List.for_all (fun (a,b) -> a<>num or pf_conv_x gl b csr) lcm) then
+      (num,csr)::(verify_metas_coherence gl lcm tl)
     else
       raise Not_coherent_metas
   | [] -> []
@@ -765,12 +764,12 @@ let apply_matching pat csr =
      PatternMatchingFailure -> raise No_match
 
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context ist lmatch mhyp lhyps noccopt =
+let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
   let get_pattern = function
     | Hyp (_,pat) -> pat
     | NoHypId pat -> pat
   and get_id_couple id = function
-    | Hyp((_,idpat),_) -> [idpat,VIdentifier id]
+    | Hyp((_,idpat),_) -> [idpat,VConstr (mkVar id)]
     | NoHypId _ -> [] in
   let rec apply_one_mhyp_context_rec mhyp lhyps_acc nocc = function
     | (id,hyp)::tl ->
@@ -778,14 +777,14 @@ let apply_one_mhyp_context ist lmatch mhyp lhyps noccopt =
       | Term t ->
         (try
           let lmeta = 
-            verify_metas_coherence ist lmatch (Pattern.matches t hyp) in
+            verify_metas_coherence gl lmatch (Pattern.matches t hyp) in
           (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None)
          with | PatternMatchingFailure | Not_coherent_metas ->
           apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl)
       | Subterm (ic,t) ->
         (try
           let (lm,ctxt) = sub_match nocc t hyp in
-          let lmeta = verify_metas_coherence ist lmatch lm in
+          let lmeta = verify_metas_coherence gl lmatch lm in
           (get_id_couple id mhyp,give_context ctxt
             ic,lmeta,tl,(id,hyp),Some nocc)
          with
@@ -800,17 +799,6 @@ let apply_one_mhyp_context ist lmatch mhyp lhyps noccopt =
     | Some n -> n in
   apply_one_mhyp_context_rec mhyp [] nocc lhyps
 
-(*
-let coerce_to_qualid loc = function
-  | Constr c when isVar c -> make_short_qualid (destVar c)
-  | Constr c -> 
-      (try qualid_of_sp (sp_of_global (Global.env()) (reference_of_constr c))
-      with Not_found -> invalid_arg_loc (loc, "Not a reference"))
-  | Identifier id -> make_short_qualid id
-  | Qualid qid -> qid
-  | _ -> invalid_arg_loc (loc, "Not a reference")
-*)
-
 let constr_to_id loc c =
   if isVar c then destVar c
   else invalid_arg_loc (loc, "Not an identifier")
@@ -820,21 +808,18 @@ let constr_to_qid loc c =
   with _ -> invalid_arg_loc (loc, "Not a global reference")
 
 (* Check for LetTac *)
-let check_clause_pattern ist (l,occl) =
-  match ist.goalopt with
-  | Some gl ->
-      let sign = pf_hyps gl in
-      let rec check acc = function
-	| (hyp,l) :: rest ->
-	    let _,hyp = skip_metaid hyp in
-	    if List.mem hyp acc then
-	      error ("Hypothesis "^(string_of_id hyp)^" occurs twice");
-	    if not (mem_named_context hyp sign) then
-	      error ("No such hypothesis: " ^ (string_of_id hyp));
-	    (hyp,l)::(check (hyp::acc) rest)
-	| [] -> []
-      in (l,check [] occl)
-  | None -> error "No goal"
+let check_clause_pattern ist gl (l,occl) =
+  let sign = pf_hyps gl in
+  let rec check acc = function
+    | (hyp,l) :: rest ->
+	let _,hyp = skip_metaid hyp in
+	if List.mem hyp acc then
+	  error ("Hypothesis "^(string_of_id hyp)^" occurs twice");
+	if not (mem_named_context hyp sign) then
+	  error ("No such hypothesis: " ^ (string_of_id hyp));
+	(hyp,l)::(check (hyp::acc) rest)
+    | [] -> []
+  in (l,check [] occl)
 
 (* Debug reference *)
 let debug = ref DebugOff
@@ -845,196 +830,196 @@ let set_debug pos = debug := pos
 (* Gives the state of debug *)
 let get_debug () = !debug
 
-(* Interprets an identifier *)
+(* Interprets an identifier which must be fresh *)
 let eval_ident ist id =
-  try (unrec (List.assoc id ist.lfun))
-  with | Not_found ->
-(*
-    try (vcontext_interp ist (lookup (make_short_qualid id)))
-    with | Not_found -> 
-*)
-VIdentifier id
-
-(* Gives the identifier corresponding to an Identifier tactic_arg *)
-let id_of_Identifier = function
-  | VConstr c when isVar c -> destVar c
-  | VConstr c ->
-      (match kind_of_term c with
-          Var id -> id
-        | Const sp -> id_of_global None (ConstRef sp)
-        | Ind sp -> id_of_global None (IndRef sp)
-        | Construct sp -> id_of_global None (ConstructRef sp)
-        | _ ->
-            anomalylabstrm "id_of_Identifier"
-              (str "Not an IDENTIFIER tactic_arg"))
+  try match List.assoc id ist.lfun with
   | VIdentifier id -> id
-  | _ ->
-    anomalylabstrm "id_of_Identifier" (str "Not an IDENTIFIER tactic_arg")
+  | _ -> user_err_loc(loc,"eval_ident",str "should be bound to an identifier")
+  with Not_found -> id
 
-let coerce_to_hypothesis ist = function
-  | VConstr c when isVar c -> destVar c
-  | VIdentifier id -> id
-  | v -> errorlabstrm "coerce_to_hypothesis"
-      (str "Cannot coerce" ++ spc () ++ pr_value ist.env v ++ spc () ++
-       str "to an existing hypothesis")
+let eval_integer lfun (loc,id) =
+  try match List.assoc id lfun with
+  | VInteger n -> ArgArg n
+  | _ -> user_err_loc(loc,"eval_integer",str "should be bound to an integer")
+  with Not_found -> user_err_loc (loc,"eval_integer",str "Unbound variable")
+
+let constr_of_value env = function
+  | VConstr csr -> csr
+  | VIdentifier id -> constr_of_id env id
+  | _ -> raise Not_found
 
-let ident_interp ist id =
-  id_of_Identifier (eval_ident ist id)
+let is_variable env id =
+  List.mem id (ids_of_named_context (Environ.named_context env))
 
-let hyp_interp ist (loc,id) =
-  coerce_to_hypothesis ist (eval_ident ist id)
+let variable_of_value env = function
+  | VConstr c as v when isVar c -> destVar c
+  | VIdentifier id' when is_variable env id' -> id'
+  | _ -> raise Not_found
 
-let name_interp ist = function
+(* Extract a variable from a value, if any *)
+let id_of_Identifier = variable_of_value
+
+(* Extract a constr from a value, if any *)
+let constr_of_VConstr = constr_of_value
+
+(* Interprets a variable *)
+let eval_variable ist gl (loc,id) =
+  (* Look first in lfun for a value coercible to a variable *)
+  try 
+    let v = List.assoc id ist.lfun in
+    try variable_of_value (pf_env gl) v
+    with Not_found ->
+      errorlabstrm "coerce_to_variable"
+      (str "Cannot coerce" ++ spc () ++ pr_value (pf_env gl) v ++ spc () ++
+      str "to a variable")
+  with Not_found -> 
+  (* Then look if bound in the proof context at calling time *)
+  if is_variable (pf_env gl) id then id
+  else
+    Pretype_errors.error_var_not_found_loc loc id
+
+let hyp_interp = eval_variable
+
+let eval_name ist = function
   | Anonymous -> Anonymous
-  | Name id -> Name (ident_interp ist id)
+  | Name id -> Name (eval_ident ist id)
 
-let hyp_or_metanum_interp ist = function
-  | AN id -> ident_interp ist id
+let hyp_or_metanum_interp ist gl = function
+  | AN id -> eval_variable ist gl (dummy_loc,id)
   | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch)
 
-(* To avoid to move to much simple functions in the big recursive block *)
-let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
-
-let interp_pure_qualid is_applied ist (loc,qid) =
-  try VConstr (constr_of_reference (find_reference ist qid))
+let interp_pure_qualid is_applied env (loc,qid) =
+  try VConstr (constr_of_reference (find_reference env qid))
   with Not_found ->
     let (dir,id) = repr_qualid qid in
     if not is_applied & dir = empty_dirpath then VIdentifier id
     else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference")
 
-let interp_ltac_qualid is_applied ist (loc,qid as lqid) =
-  try (!forward_vcontext_interp ist (lookup qid))
-  with Not_found -> interp_pure_qualid is_applied ist lqid
-
-let interp_ltac_reference isapplied ist = function
-  | Ident (loc,id) -> 
-      (try unrec (List.assoc id ist.lfun)
-      with | Not_found ->
-        interp_ltac_qualid isapplied ist (loc,make_short_qualid id))
-  | Qualid qid -> interp_ltac_qualid isapplied ist qid
-
 (* Interprets a qualified name *)
-let eval_ref ist = function
-  | Qualid locqid -> interp_pure_qualid false ist locqid
+let eval_ref ist env = function
+  | Qualid locqid -> interp_pure_qualid false env locqid
   | Ident (loc,id) ->
       try unrec (List.assoc id ist.lfun)
-      with Not_found -> interp_pure_qualid false ist (loc,make_short_qualid id)
+      with Not_found -> interp_pure_qualid false env (loc,make_short_qualid id)
+
+let reference_interp ist env qid =
+  let v = eval_ref ist env qid in
+  coerce_to_reference env v
 
-let reference_interp ist qid =
-  let v = eval_ref ist qid in
-  coerce_to_reference ist v
+let pf_reference_interp ist gl = reference_interp ist (pf_env gl)
 
 (* Interprets a qualified name. This can be a metavariable to be injected *)
 let qualid_or_metanum_interp ist = function
   | AN qid -> qid
   | MetaNum (loc,n) -> constr_to_qid loc (List.assoc n ist.lmatch)
 
-let eval_ref_or_metanum ist = function
-  | AN qid -> eval_ref ist qid
+let eval_ref_or_metanum ist gl = function
+  | AN qid -> eval_ref ist gl qid
   | MetaNum (loc,n) -> VConstr (List.assoc n ist.lmatch)
 
-let interp_evaluable_or_metanum ist c =
-  let c = eval_ref_or_metanum ist c in
-  coerce_to_evaluable_ref ist.env c
+let interp_evaluable_or_metanum ist env c =
+  let c = eval_ref_or_metanum ist env c in
+  coerce_to_evaluable_ref env c
 
-let interp_inductive_or_metanum ist c =
-  let c = eval_ref_or_metanum ist c in
+let interp_inductive_or_metanum ist gl c =
+  let c = eval_ref_or_metanum ist (pf_env gl) c in
   coerce_to_inductive c
 
 (* Interprets an hypothesis name *)
-let interp_hyp_location ist = function
-  | InHyp id -> InHyp (hyp_interp ist (skip_metaid id))
-  | InHypType id -> InHypType (hyp_interp ist (skip_metaid id))
+let interp_hyp_location ist gl = function
+  | InHyp id -> InHyp (hyp_interp ist gl (skip_metaid id))
+  | InHypType id -> InHypType (hyp_interp ist gl (skip_metaid id))
 
-let id_opt_interp ist = option_app (ident_interp ist)
+let eval_opt_ident ist = option_app (eval_ident ist)
 
 (* Interpretation of constructions *)
 
-  (* Extracted the constr list from lfun *)
-let rec constr_list_aux ist = function
-  | (id,VConstr c)::tl -> (id,c)::(constr_list_aux ist tl)
-  | (id0,VIdentifier id)::tl ->
-    (try (id0,(constr_of_id ist id))::(constr_list_aux ist tl)
-     with | Not_found -> (constr_list_aux ist tl))
-  | _::tl -> constr_list_aux ist tl
-  | [] -> []
+(* Extracted the constr list from lfun *)
+let rec constr_list_aux env = function
+  | (id,v)::tl -> 
+      let (l1,l2) = constr_list_aux env tl in
+      (try ((id,constr_of_value env v)::l1,l2)
+       with Not_found -> 
+	 (l1,(id,match v with VIdentifier id0 -> Some id0 | _ -> None)::l2))
+  | [] -> ([],[])
+
+let constr_list ist env = constr_list_aux env ist.lfun
+
+let interp_constr ocl ist sigma env c =
+  interp_constr_gen sigma env (constr_list ist env) ist.lmatch c ocl
 
-let constr_list ist = constr_list_aux ist ist.lfun
-let interp_constr ocl ist c =
-  interp_constr_gen ist.evc ist.env (constr_list ist) ist.lmatch c ocl
+let interp_openconstr ist gl c ocl =
+  interp_openconstr_gen (project gl) (pf_env gl)
+    (constr_list ist (pf_env gl)) ist.lmatch c ocl
 
-let interp_openconstr ist c ocl =
-  interp_openconstr_gen ist.evc ist.env (constr_list ist) ist.lmatch c ocl
+let pf_interp_constr ist gl =
+  interp_constr None ist (project gl) (pf_env gl)
 
 (* Interprets a constr expression *)
-let constr_interp ist c =
-  let csr = interp_constr None ist c in
+let constr_interp ist sigma env c =
+  let csr = interp_constr None ist sigma env c in
   begin
-    db_constr ist.debug ist.env csr;
+    db_constr ist.debug env csr;
     csr
   end
 
+let pf_constr_interp ist gl c = constr_interp ist (project gl) (pf_env gl) c
+
 (* Interprets a constr expression casted by the current goal *)
-let cast_constr_interp ist c =
-  match ist.goalopt with
-  | Some gl ->
-      let csr = interp_constr (Some (pf_concl gl)) ist c in
-      begin
-	db_constr ist.debug ist.env csr;
-	csr
-      end
-
-  | None ->
-      errorlabstrm "cast_constr_interp" 
-      (str "Cannot cast a constr without goal")
+let cast_constr_interp ist gl c =
+  let csr = interp_constr (Some (pf_concl gl)) ist (project gl) (pf_env gl) c in
+  db_constr ist.debug (pf_env gl) csr;
+  csr
 
 (* Interprets an open constr expression casted by the current goal *)
-let cast_openconstr_interp ist c =
-  match ist.goalopt with
-  | Some gl -> interp_openconstr ist c (Some (pf_concl gl))
-  | None ->
-    errorlabstrm "cast_openconstr_interp"
-      (str "Cannot cast a constr without goal")
+let cast_openconstr_interp ist gl c =
+  interp_openconstr ist gl c (Some (pf_concl gl))
 
 (* Interprets a reduction expression *)
-let unfold_interp ist (l,qid) = (l,interp_evaluable_or_metanum ist qid)
+let unfold_interp ist env (l,qid) =
+  (l,interp_evaluable_or_metanum ist env qid)
+
+let flag_interp ist env red =
+  { red
+    with rConst = List.map (interp_evaluable_or_metanum ist env) red.rConst }
 
-let flag_interp ist red =
-  { red with rConst = List.map (interp_evaluable_or_metanum ist) red.rConst }
+let pattern_interp ist sigma env (l,c) = (l,constr_interp ist sigma env c)
 
-let pattern_interp ist (l,c) = (l,constr_interp ist c)
+let pf_pattern_interp ist gl = pattern_interp ist (project gl) (pf_env gl)
 
-let redexp_interp ist = function
-  | Unfold l -> Unfold (List.map (unfold_interp ist) l)
-  | Fold l -> Fold (List.map (constr_interp ist) l)
-  | Cbv f -> Cbv (flag_interp ist f)
-  | Lazy f -> Lazy (flag_interp ist f)
-  | Pattern l -> Pattern (List.map (pattern_interp ist) l)
-  | Simpl o -> Simpl (option_app (pattern_interp ist) o)
+let redexp_interp ist sigma env = function
+  | Unfold l -> Unfold (List.map (unfold_interp ist env) l)
+  | Fold l -> Fold (List.map (constr_interp ist sigma env) l)
+  | Cbv f -> Cbv (flag_interp ist env f)
+  | Lazy f -> Lazy (flag_interp ist env f)
+  | Pattern l -> Pattern (List.map (pattern_interp ist sigma env) l)
+  | Simpl o -> Simpl (option_app (pattern_interp ist sigma env) o)
   | (Red _ |  Hnf as r) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s,constr_interp ist c)
+  | ExtraRedExpr (s,c) -> ExtraRedExpr (s,constr_interp ist sigma env c)
+
+let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
 
-let interp_may_eval f ist = function
+let interp_may_eval f ist gl = function
   | ConstrEval (r,c) ->
-      let redexp = redexp_interp ist r in
-      (reduction_of_redexp redexp) ist.env ist.evc (f ist c)
+      let redexp = pf_redexp_interp ist gl  r in
+      pf_reduction_of_redexp gl redexp (f ist gl c)
   | ConstrContext ((loc,s),c) ->
       (try
-	let ic = f ist c
+	let ic = f ist gl c
 	and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in
 	subst_meta [-1,ic] ctxt
       with
 	| Not_found ->
 	    user_err_loc (loc, "constr_interp",
 	    str "Unbound context identifier" ++ pr_id s))
-  | ConstrTypeOf c -> type_of ist.env ist.evc (f ist c)
-  | ConstrTerm c -> f ist c
+  | ConstrTypeOf c -> pf_type_of gl (f ist gl c)
+  | ConstrTerm c -> f ist gl c
 
 (* Interprets a constr expression possibly to first evaluate *)
-let constr_interp_may_eval ist c =
-  let csr = interp_may_eval (interp_constr None) ist c in
+let constr_interp_may_eval ist gl c =
+  let csr = interp_may_eval pf_interp_constr ist gl c in
   begin
-    db_constr ist.debug ist.env csr;
+    db_constr ist.debug (pf_env gl) csr;
     csr
   end
 
@@ -1044,72 +1029,67 @@ let rec interp_intro_pattern ist = function
   | IntroWildcard ->
       IntroWildcard
   | IntroIdentifier id ->
-      IntroIdentifier (ident_interp ist id)
+      IntroIdentifier (eval_ident ist id)
 
-let interp_quantified_hypothesis ist = function
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let interp_quantified_hypothesis ist gl = function
   | AnonHyp n -> AnonHyp n
-  | NamedHyp id -> 
-      match eval_ident ist id with
+  | NamedHyp id ->
+      try match List.assoc id ist.lfun with
 	| VInteger n -> AnonHyp n
-	| v -> NamedHyp (coerce_to_hypothesis ist v)
+	| VIdentifier id -> NamedHyp id
+	| v -> NamedHyp (variable_of_value (pf_env gl) v)
+      with Not_found -> NamedHyp id
 
-let interp_induction_arg ist = function
-  | ElimOnConstr c -> ElimOnConstr (constr_interp ist c)
+let interp_induction_arg ist gl = function
+  | ElimOnConstr c -> ElimOnConstr (pf_constr_interp ist gl c)
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (loc,id) ->
-      match ist.goalopt with
-      | None -> error "No goal"
-      | Some gl ->
-	  if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
-	  else ElimOnConstr
-(*	    (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))*)
-	    (constr_interp ist (CRef (Ident (loc,id))))
-
-let binding_interp ist (loc,b,c) =
-  (loc,interp_quantified_hypothesis ist b,constr_interp ist c)
-
-let bindings_interp ist = function
-  | NoBindings -> NoBindings
-  | ImplicitBindings l -> ImplicitBindings (List.map (constr_interp ist) l)
-  | ExplicitBindings l -> ExplicitBindings (List.map (binding_interp ist) l)
+      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+      else ElimOnConstr	(pf_constr_interp ist gl (CRef (Ident (loc,id))))
+
+let binding_interp ist gl (loc,b,c) =
+  (loc,interp_quantified_hypothesis ist gl b,pf_constr_interp ist gl c)
 
-let interp_constr_with_bindings ist (c,bl) =
-  (constr_interp ist c, bindings_interp ist bl)
+let bindings_interp ist gl = function
+| NoBindings -> NoBindings
+| ImplicitBindings l -> ImplicitBindings (List.map (pf_constr_interp ist gl) l)
+| ExplicitBindings l -> ExplicitBindings (List.map (binding_interp ist gl) l)
 
-(* Interprets a tactic expression *)
-let rec val_interp ist ast =
+let interp_constr_with_bindings ist gl (c,bl) =
+  (pf_constr_interp ist gl c, bindings_interp ist gl bl)
+
+(* Interprets a l-tac expression into a value *)
+let rec val_interp ist gl tac =
 
   let value_interp ist =
-    match ast with
+    match tac with
     (* Immediate evaluation *)
     | TacFun (it,body) -> VFun (ist.lfun,it,body)
-    | TacFunRec rc -> funrec_interp ist rc
-    | TacLetRecIn (lrc,u) -> letrec_interp ist lrc u
+    | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u
     | TacLetIn (l,u) ->
-        let addlfun=letin_interp ist l in
-        val_interp { ist with lfun=addlfun@ist.lfun } u
-    | TacMatchContext (lr,lmr) ->
-       (match ist.goalopt with
-          | None -> VContext (ist,lr,lmr)
-          | Some g -> match_context_interp ist lr lmr g)
-    | TacMatch (c,lmr) -> match_interp ist c lmr
-    | TacArg a -> tacarg_interp ist a
+        let addlfun = letin_interp ist gl l in
+        val_interp { ist with lfun=addlfun@ist.lfun } gl u
+    | TacMatchContext (lr,lmr) -> match_context_interp ist gl lr lmr
+    | TacMatch (c,lmr) -> match_interp ist gl c lmr
+    | TacArg a -> tacarg_interp ist gl a
     (* Delayed evaluation *)
-    | t -> VClosure (ist,t) 
+    | t -> VTactic (eval_tactic ist t)
+
  in
-  if ist.debug = DebugOn then
-    match debug_prompt ist.goalopt ast with
-    | Exit -> VClosure (ist,TacId)
-    | v -> value_interp {ist with debug=v}
-  else
-    value_interp ist
+  match ist.debug with
+    | DebugOn n ->
+	debug_prompt n (Some gl) tac
+	(fun v -> value_interp {ist with debug=v})
+	(fun () -> VTactic tclIDTAC)
+    | _ -> value_interp ist
 
 and eval_tactic ist = function
   | TacAtom (loc,t) -> fun gl ->
-      (try interp_atomic ist t gl
+      (try (interp_atomic ist gl t) gl
        with e -> Stdpp.raise_with_loc loc e)
   | TacFun (it,body) -> assert false
-  | TacFunRec rc -> assert false
   | TacLetRecIn (lrc,u) -> assert false
   | TacLetIn (l,u) -> assert false
   | TacLetCut l -> letcut_interp ist l
@@ -1130,19 +1110,24 @@ and eval_tactic ist = function
         tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2)
   | TacFirst l -> tclFIRST (List.map (tactic_interp ist) l)
   | TacSolve l -> tclSOLVE (List.map (tactic_interp ist) l)
-(* Obsolete ??
-    | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
-          (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
-    | Node(_,"PRIMTACTIC",[Node(loc,opn,[])]) ->
-        VFTactic ([],(interp_atomic opn))
-*)
   | TacArg a -> assert false
 
-and tacarg_interp ist = function
+and interp_ltac_qualid is_applied ist gl (loc,qid as lqid) =
+  try val_interp ist gl (lookup qid)
+  with Not_found -> interp_pure_qualid is_applied (pf_env gl) lqid
+
+and interp_ltac_reference isapplied ist gl = function
+  | Ident (loc,id) -> 
+      (try unrec (List.assoc id ist.lfun)
+      with | Not_found ->
+        interp_ltac_qualid isapplied ist gl (loc,make_short_qualid id))
+  | Qualid qid -> interp_ltac_qualid isapplied ist gl qid
+
+and tacarg_interp ist gl = function
   | TacVoid -> VVoid
-  | Reference r -> interp_ltac_reference false ist r
+  | Reference r -> interp_ltac_reference false ist gl r
   | Integer n -> VInteger n
-  | ConstrMayEval c -> VConstr (constr_interp_may_eval ist c)
+  | ConstrMayEval c -> VConstr (constr_interp_may_eval ist gl c)
   | MetaNumArg (_,n) -> VConstr (List.assoc n ist.lmatch)
   | MetaIdArg (loc,id) ->
       (try (* $id can occur in Grammar tactic... *)
@@ -1150,17 +1135,15 @@ and tacarg_interp ist = function
       with
         | Not_found -> error_syntactic_metavariables_not_allowed loc)
   | TacCall (loc,f,l) ->
-      let fv = interp_ltac_reference true ist f
-      and largs = List.map (tacarg_interp ist) l in
-      app_interp ist fv largs loc
-  | Tacexp t -> val_interp ist t
-(*
-  | Tacexp t -> VArg (Tacexp ((*tactic_interp ist t,*)t))
-*)
+      let fv = interp_ltac_reference true ist gl f
+      and largs = List.map (tacarg_interp ist gl) l in
+      List.iter check_is_value largs;
+      app_interp ist gl fv largs loc
+  | Tacexp t -> val_interp ist gl t
   | TacDynamic(_,t) ->
       let tg = (tag t) in
       if tg = "tactic" then
-        let f = (tactic_out t) in val_interp ist (f ist)
+        let f = (tactic_out t) in val_interp ist gl (f ist)
       else if tg = "value" then
         value_out t
       else if tg = "constr" then
@@ -1170,17 +1153,13 @@ and tacarg_interp ist = function
           (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
 
 (* Interprets an application node *)
-and app_interp ist fv largs loc =
+and app_interp ist gl fv largs loc =
   match fv with
-    | VFTactic(l,f) -> VFTactic(l@largs,f)
     | VFun(olfun,var,body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
-        if lval=[] then
-          val_interp { ist with lfun=newlfun@olfun } body
-        else
-          app_interp ist
-            (val_interp {ist with lfun=newlfun@olfun } body) lval loc
+	let v = val_interp { ist with lfun=newlfun@olfun } gl body in
+        if lval=[] then v else app_interp ist gl v lval loc
       else
         VFun(newlfun@olfun,lvar,body)
     | _ ->
@@ -1190,19 +1169,15 @@ and app_interp ist fv largs loc =
 (* Gives the tactic corresponding to the tactic value *)
 and tactic_of_value vle g =
   match vle with
-  | VClosure (ist,tac) -> eval_tactic ist tac g
-  | VFTactic (largs,f) -> (f largs g) 
   | VRTactic res -> res
   | VTactic tac -> tac g
   | VFun _ -> error "A fully applied tactic is expected"
   | _ -> raise NotTactic
 
 (* Evaluation with FailError catching *)
-and eval_with_fail interp ast goal =
+and eval_with_fail interp tac goal =
   try 
-    (match interp ast with
-    | VClosure (ist,tac) -> VRTactic (eval_tactic ist tac goal)
-    | VFTactic (largs,f) -> VRTactic (f largs goal)
+    (match interp goal tac with
     | VTactic tac -> VRTactic (tac goal)
     | a -> a)
   with | FailError lvl ->
@@ -1212,241 +1187,179 @@ and eval_with_fail interp ast goal =
       raise (FailError (lvl - 1))
 
 (* Interprets recursive expressions *)
-and funrec_interp ist ((loc,name),(var,body)) =
-    let ve = ref VVoid in
-    let newve = VFun((name,VRec ve)::ist.lfun,var,body) in
-    begin
-      ve:=newve;
-      !ve
-    end
-
-and letrec_interp ist lrc u =
-    let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
-    let lenv = List.fold_right2 (fun ((loc,name),_) vref l -> (name,VRec vref)::l)
+and letrec_interp ist gl lrc u =
+  let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
+  let lenv =
+    List.fold_right2 (fun ((loc,name),_) vref l -> (name,VRec vref)::l)
       lrc lref [] in
-    let lve = List.map (fun ((loc,name),(var,body)) ->
+  let lve = List.map (fun ((loc,name),(var,body)) ->
                           (name,VFun(lenv@ist.lfun,var,body))) lrc in
-    begin
-      List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
-      val_interp { ist with lfun=lve@ist.lfun } u
-    end
+  begin
+    List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
+    val_interp { ist with lfun=lve@ist.lfun } gl u
+  end
 
-(* Interprets the clauses of a LetCutIn *)
-and letin_interp ist = function
+(* Interprets the clauses of a LetIn *)
+and letin_interp ist gl = function
   | [] -> []
-  | ((loc,id),None,t)::tl -> (id,tacarg_interp ist t):: (letin_interp ist tl)
+  | ((loc,id),None,t)::tl -> 
+      let v = tacarg_interp ist gl t in
+      check_is_value v;
+      (id,v):: (letin_interp ist gl tl)
+
   | ((loc,id),Some com,tce)::tl ->
-    let typ = interp_may_eval (interp_constr None) ist com
-    and tac = tacarg_interp ist tce in
-    match tac with
-    | VConstr csr ->
-      (id,VConstr (mkCast (csr,typ)))::(letin_interp ist tl)
-    | VIdentifier id ->
-      (try
-         (id,VConstr (mkCast (constr_of_id ist id,typ)))::
-         (letin_interp ist tl)
-       with | Not_found ->
-         errorlabstrm "Tacinterp.letin_interp"
-         (str "Term or tactic expected"))
-    | _ ->
-      (try
-         let t = tactic_of_value tac in
-         let ndc =
-           (match ist.goalopt with
-           | None -> Global.named_context ()
-           | Some g -> pf_hyps g) in
-         start_proof id IsLocal ndc typ (fun _ _ -> ());
-         by t;
-         let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
-           cook_proof () in
-         delete_proof (dummy_loc,id);
-         (id,VConstr (mkCast (pft,typ)))::(letin_interp ist tl)
-       with | NotTactic ->
-         delete_proof (dummy_loc,id);
-         errorlabstrm "Tacinterp.letin_interp"
-         (str "Term or fully applied tactic expected in Let"))
+    let typ = interp_may_eval pf_interp_constr ist gl com
+    and v = tacarg_interp ist gl tce in
+    let csr = 
+      try
+	constr_of_value (pf_env gl) v
+      with Not_found ->
+      try
+	let t = tactic_of_value v in
+	let ndc = Environ.named_context (pf_env gl) in
+	start_proof id IsLocal ndc typ (fun _ _ -> ());
+	by t;
+	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
+	delete_proof (dummy_loc,id);
+        pft
+      with | NotTactic ->
+	delete_proof (dummy_loc,id);
+	errorlabstrm "Tacinterp.letin_interp"
+          (str "Term or fully applied tactic expected in Let")
+    in (id,VConstr (mkCast (csr,typ)))::(letin_interp ist gl tl)
 
 (* Interprets the clauses of a LetCut *)
-and letcut_interp ist = function
+and letcut_interp ist = function 
   | [] -> tclIDTAC
-  | (id,com,tce)::tl ->
-    let typ = constr_interp_may_eval ist com
-    and tac = tacarg_interp ist tce
-    and (ndc,ccl) =
-      match ist.goalopt with
-      |	None -> 
-        errorlabstrm "Tacinterp.letcut_interp" (str
-        "Do not use Let for toplevel definitions, use Lemma, ... instead")
-      |	Some g -> (pf_hyps g,pf_concl g) in
-    (match tac with
-    | VConstr csr ->
-      let cutt = h_cut typ
-      and exat = h_exact csr in
-      tclTHENSV cutt [|tclTHEN (introduction id)
-      (letcut_interp ist tl);exat|]
+  | (id,c,tce)::tl -> fun gl ->
+    let typ = constr_interp_may_eval ist gl c
+    and v = tacarg_interp ist gl tce in
+    let csr = 
+      try
+	constr_of_value (pf_env gl) v
+      with Not_found ->
+      try
+	let t = tactic_of_value v in
+	start_proof id IsLocal (pf_hyps gl) typ (fun _ _ -> ());
+	by t;
+	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
+	delete_proof (dummy_loc,id);
+        pft
+      with | NotTactic ->
+	delete_proof (dummy_loc,id);
+	errorlabstrm "Tacinterp.letin_interp"
+          (str "Term or fully applied tactic expected in Let")
+    in
+    let cutt = h_cut typ
+    and exat = h_exact csr in
+    tclTHENSV cutt [|tclTHEN (introduction id) (letcut_interp ist tl);exat|] gl
 
 (*      let lic = mkLetIn (Name id,csr,typ,ccl) in
       let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in
       tclTHEN ntac (tclTHEN (introduction id)
       (letcut_interp ist tl))*)
 
-    | VIdentifier ir ->
-      (try
-         let cutt = h_cut typ
-         and exat = h_exact (constr_of_id ist ir) in
-         tclTHENSV cutt [| tclTHEN (introduction id) 
-	 (letcut_interp ist tl); exat |]
-       with | Not_found ->
-         errorlabstrm "Tacinterp.letin_interp"
-         (str "Term or tactic expected"))
-    | _ ->
-      (try
-         let t = tactic_of_value tac in
-         start_proof id IsLocal ndc typ (fun _ _ -> ());
-         by t;
-         let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
-           cook_proof () in
-         delete_proof (dummy_loc,id);
-         let cutt = h_cut typ
-         and exat = h_exact pft in
-         tclTHENSV cutt [|tclTHEN (introduction id)
-         (letcut_interp ist tl);exat|]
-
-(*         let lic = mkLetIn (Name id,pft,typ,ccl) in
-         let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in
-         tclTHEN ntac (tclTHEN (introduction id)
-         (letcut_interp ist tl))*)
-       with | NotTactic ->
-         delete_proof (dummy_loc,id);
-         errorlabstrm "Tacinterp.letcut_interp"
-         (str "Term or fully applied tactic expected in Let")))
-
 (* Interprets the Match Context expressions *)
-and match_context_interp ist lr lmr g =
-(*  let goal =
-    (match goalopt with
-    | None ->
-      errorlabstrm "Tacinterp.apply_match_context" (str
-        "No goal available")
-    | Some g -> g) in*)
-  let rec apply_goal_sub ist goal nocc (id,c) csr mt mhyps hyps =
+and match_context_interp ist goal lr lmr =
+  let rec apply_goal_sub ist nocc (id,c) csr mt mhyps hyps =
     try
       let (lgoal,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
       if mhyps = [] then
         eval_with_fail
-          (val_interp
-            { ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch;
-                       goalopt=Some goal})
+          (val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch})
           mt goal
       else
-        apply_hyps_context {ist with goalopt=Some goal} mt lgoal mhyps hyps
+        apply_hyps_context ist goal mt lgoal mhyps hyps
     with
     | (FailError _) as e -> raise e
     | NextOccurrence _ -> raise No_match
     | No_match | _ ->
-      apply_goal_sub ist goal (nocc + 1) (id,c) csr mt mhyps hyps in
-  let rec apply_match_context ist goal = function
+      apply_goal_sub ist (nocc + 1) (id,c) csr mt mhyps hyps in
+  let rec apply_match_context ist = function
     | (All t)::tl ->
       (try
-         eval_with_fail (val_interp {ist with goalopt=Some goal }) t
-           goal
-       with No_match | FailError _ -> apply_match_context ist goal tl
-	 | e when Logic.catchable_exception e -> apply_match_context ist goal tl)
+         eval_with_fail (val_interp ist) t goal
+       with No_match | FailError _ -> apply_match_context ist tl
+	 | e when Logic.catchable_exception e -> apply_match_context ist tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
       let hyps = make_hyps (pf_hyps goal) in
       let hyps = if lr then List.rev hyps else hyps in
+      let mhyps = List.rev mhyps (* Sens naturel *) in
       let concl = pf_concl goal in
       (match mgoal with
       |	Term mg ->
         (try
            (let lgoal = apply_matching mg concl in
             begin
-            db_matched_concl ist.debug ist.env concl;
+            db_matched_concl ist.debug (pf_env goal) concl;
             if mhyps = [] then
-              eval_with_fail (val_interp
-                {ist with lmatch=lgoal@ist.lmatch; goalopt=Some goal}) mt goal
+              eval_with_fail
+		(val_interp {ist with lmatch=lgoal@ist.lmatch}) mt goal
             else
-              apply_hyps_context { ist with goalopt=Some goal} mt lgoal mhyps
-                hyps
+              apply_hyps_context ist goal mt lgoal mhyps hyps
             end)
-        with e when is_match_catchable e -> apply_match_context ist goal tl)
+        with e when is_match_catchable e -> apply_match_context ist tl)
       |	Subterm (id,mg) ->
         (try
-          apply_goal_sub ist goal 0 (id,mg) concl mt mhyps hyps
+          apply_goal_sub ist 0 (id,mg) concl mt mhyps hyps
         with e when is_match_catchable e ->
-	  apply_match_context ist goal tl))
+	  apply_match_context ist tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match_context" (str
         "No matching clauses for Match Context")
 
   in
-  apply_match_context ist g
-    (read_match_rule ist.evc ist.env (constr_list ist) lmr)
-
-(* Interprets a VContext value *)
-and vcontext_interp ist = function
-  | (VContext (ist',lr,lmr)) as v ->
-    (match ist.goalopt with
-    | None -> v
-    | Some g as go -> 
-        let ist = { ist' with goalopt = go; env = pf_env g; evc = project g }
-        in match_context_interp ist lr lmr g)
-  | v -> v
+  let env = pf_env goal in
+  apply_match_context ist 
+    (read_match_rule (project goal) env (constr_list ist env) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist mt lgmatch mhyps hyps =
-  let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp
+and apply_hyps_context ist goal mt lgmatch mhyps hyps =
+  let rec apply_hyps_context_rec mt lfun lmatch mhyps lhyps_mhyp
     lhyps_rest noccopt =
-  let goal = match ist.goalopt with Some g -> g | _ -> assert false in 
     match mhyps with
       | hd::tl ->
         let (lid,lc,lm,newlhyps,hyp_match,noccopt) =
-          apply_one_mhyp_context ist lmatch hd lhyps_mhyp noccopt in
+          apply_one_mhyp_context goal lmatch hd lhyps_mhyp noccopt in
         begin
-        db_matched_hyp ist.debug ist.env hyp_match;
+        db_matched_hyp ist.debug (pf_env goal) hyp_match;
         (try
         if tl = [] then
             eval_with_fail
               (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
-                                    lmatch=lmatch@lm@ist.lmatch;
-                                    goalopt=Some goal})
+                                    lmatch=lmatch@lm@ist.lmatch})
               mt goal
         else
           let nextlhyps =
             List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
               lhyps_rest in
-          apply_hyps_context_rec ist mt
+          apply_hyps_context_rec mt
             (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
          with
         | (FailError _) as e -> raise e
 	|  e when is_match_catchable e -> 
           (match noccopt with
           | None ->
-            apply_hyps_context_rec ist mt lfun
+            apply_hyps_context_rec mt lfun
               lmatch mhyps newlhyps lhyps_rest None
           | Some nocc ->
-            apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps
+            apply_hyps_context_rec mt ist.lfun ist.lmatch mhyps
               (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
         end
       |	[] ->
         anomalylabstrm "apply_hyps_context_rec" (str
           "Empty list should not occur") in
-  apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
+  apply_hyps_context_rec mt [] lgmatch mhyps hyps hyps None
 
   (* Interprets extended tactic generic arguments *)
-and genarg_interp ist x =
+and genarg_interp ist goal x =
   match genarg_tag x with
   | BoolArgType -> in_gen wit_bool (out_gen rawwit_bool x)
   | IntArgType -> in_gen wit_int (out_gen rawwit_int x)
   | IntOrVarArgType ->
       let f = function
-	| ArgVar (loc,id) ->
-	    (match eval_ident ist id with
-	      | VInteger n -> ArgArg n
-	      | _ ->
-		  user_err_loc 
-		    (loc,"genarg_interp",str "should be bound to an integer"))
+	| ArgVar locid -> eval_integer ist.lfun locid
 	| ArgArg n as x -> x in
       in_gen wit_int_or_var (f (out_gen rawwit_int_or_var x))
   | StringArgType ->
@@ -1454,251 +1367,217 @@ and genarg_interp ist x =
   | PreIdentArgType ->
       in_gen wit_pre_ident (out_gen rawwit_pre_ident x)
   | IdentArgType ->
-      in_gen wit_ident (ident_interp ist (out_gen rawwit_ident x))
+      in_gen wit_ident (out_gen rawwit_ident x)
   | RefArgType ->
-      in_gen wit_ref (reference_interp ist (out_gen rawwit_ref x))
+      in_gen wit_ref (pf_reference_interp ist goal (out_gen rawwit_ref x))
   | SortArgType ->
       in_gen wit_sort
         (destSort 
-	  (constr_interp ist (CSort (dummy_loc,out_gen rawwit_sort x))))
+	  (pf_constr_interp ist goal (CSort (dummy_loc,out_gen rawwit_sort x))))
   | ConstrArgType ->
-      in_gen wit_constr (constr_interp ist (out_gen rawwit_constr x))
+      in_gen wit_constr (pf_constr_interp ist goal (out_gen rawwit_constr x))
   | ConstrMayEvalArgType ->
-      in_gen wit_constr_may_eval (constr_interp_may_eval ist (out_gen rawwit_constr_may_eval x))
+      in_gen wit_constr_may_eval (constr_interp_may_eval ist goal (out_gen rawwit_constr_may_eval x))
   | QuantHypArgType ->
       in_gen wit_quant_hyp
-        (interp_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
+        (interp_quantified_hypothesis ist goal (out_gen rawwit_quant_hyp x))
   | RedExprArgType ->
-      in_gen wit_red_expr (redexp_interp ist (out_gen rawwit_red_expr x))
-  | TacticArgType ->
-      in_gen wit_tactic ((*tactic_interp ist*) (out_gen rawwit_tactic x))
+      in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen rawwit_red_expr x))
+  | TacticArgType -> in_gen wit_tactic (out_gen rawwit_tactic x)
   | CastedOpenConstrArgType ->
       in_gen wit_casted_open_constr 
-        (cast_openconstr_interp ist (out_gen rawwit_casted_open_constr x))
+        (cast_openconstr_interp ist goal (out_gen rawwit_casted_open_constr x))
   | ConstrWithBindingsArgType ->
       in_gen wit_constr_with_bindings
-        (interp_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
-  | List0ArgType _ -> app_list0 (genarg_interp ist) x
-  | List1ArgType _ -> app_list1 (genarg_interp ist) x
-  | OptArgType _ -> app_opt (genarg_interp ist) x
-  | PairArgType _ -> app_pair (genarg_interp ist) (genarg_interp ist) x
-  | ExtraArgType s -> lookup_genarg_interp s ist x
+        (interp_constr_with_bindings ist goal (out_gen rawwit_constr_with_bindings x))
+  | List0ArgType _ -> app_list0 (genarg_interp ist goal) x
+  | List1ArgType _ -> app_list1 (genarg_interp ist goal) x
+  | OptArgType _ -> app_opt (genarg_interp ist goal) x
+  | PairArgType _ -> app_pair (genarg_interp ist goal) (genarg_interp ist goal) x
+  | ExtraArgType s -> lookup_genarg_interp s ist goal x
 
 (* Interprets the Match expressions *)
-and match_interp ist constr lmr =
-  let rec apply_sub_match ist nocc (id,c) csr
-    mt =
-    match ist.goalopt with
-    | None ->
-      (try 
-        let (lm,ctxt) = sub_match nocc c csr in
-        let lctxt = give_context ctxt id in
-        val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} mt
-       with | NextOccurrence _ -> raise No_match)
-    | Some g ->
-      (try
-        let (lm,ctxt) = sub_match nocc c csr in
-        let lctxt = give_context ctxt id in
-        eval_with_fail (val_interp { ist with lfun=lctxt@ist.lfun;
-                                              lmatch=lm@ist.lmatch})
-          mt g
-       with
-       | NextOccurrence n -> raise No_match
-       | (FailError _) as e -> raise e
-       | e when is_match_catchable e ->
-	   apply_sub_match ist (nocc + 1) (id,c) csr mt)
+and match_interp ist g constr lmr =
+  let rec apply_sub_match ist nocc (id,c) csr mt =
+    try
+      let (lm,ctxt) = sub_match nocc c csr in
+      let lctxt = give_context ctxt id in
+      eval_with_fail 
+	(val_interp { ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch})
+        mt g
+    with
+      | NextOccurrence n -> raise No_match
+      | (FailError _) as e -> raise e
+      | e when is_match_catchable e ->
+	  apply_sub_match ist (nocc + 1) (id,c) csr mt
   in
   let rec apply_match ist csr = function
     | (All t)::_ ->
-      (match ist.goalopt with
-        | None ->
-          (try val_interp ist t
-           with e when is_match_catchable e -> apply_match ist csr [])
-        | Some g ->
-          (try
-            eval_with_fail (val_interp ist) t g
-           with
-           | (FailError _) as e -> raise e
-	   | e when is_match_catchable e -> 
-	       apply_match ist csr []))
-    | (Pat ([],mp,mt))::tl ->
-      (match mp with
-      |	Term c ->
-        (match ist.goalopt with
-        | None ->
-          (try
-             val_interp
-               { ist with lmatch=(apply_matching c csr)@ist.lmatch } mt
-           with e when is_match_catchable e -> apply_match ist csr tl)
-        | Some g ->
-          (try
-            eval_with_fail (val_interp
-              { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g
-           with
-           | (FailError _) as e -> raise e
-           | e when is_match_catchable e ->
-	       apply_match ist csr tl))
-      |	Subterm (id,c) ->
         (try
-           apply_sub_match ist 0 (id,c) csr mt
+          eval_with_fail (val_interp ist) t g
+        with
+          | (FailError _) as e -> raise e
+	  | e when is_match_catchable e -> apply_match ist csr [])
+    | (Pat ([],Term c,mt))::tl ->
+        (try
+	  eval_with_fail (val_interp
+	    { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g
+         with
+	   | (FailError _) as e -> raise e
+	   | e when is_match_catchable e -> apply_match ist csr tl)
+    | (Pat ([],Subterm (id,c),mt))::tl ->
+        (try
+          apply_sub_match ist 0 (id,c) csr mt
          with | No_match ->
-           apply_match ist csr tl))
+	   apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for Match") in
-  let csr = constr_interp_may_eval ist constr
-  and ilr = read_match_rule ist.evc ist.env (constr_list ist) lmr in
+  let csr = constr_interp_may_eval ist g constr in
+  let env = pf_env g in
+  let ilr = read_match_rule (project g) env (constr_list ist env) lmr in
   apply_match ist csr ilr
 
-and tactic_interp ist (ast:raw_tactic_expr) g =
-  tac_interp ist.lfun ist.lmatch ist.debug ast g
-
-(* Interprets tactic expressions *)
-and tac_interp lfun lmatch debug ast g =
-  let evc = project g
-  and env = pf_env g in
-  let ist = { evc=evc; env=env; lfun=lfun; lmatch=lmatch;
-              goalopt=Some g; debug=debug } in
-  try tactic_of_value (val_interp ist ast) g
+(* Interprets tactic expressions : returns a "tactic" *)
+and tactic_interp ist tac g =
+  try tactic_of_value (val_interp ist g tac) g
   with | NotTactic ->
     errorlabstrm "Tacinterp.tac_interp" (str
       "Must be a command or must give a tactic value")
 
-(*    errorlabstrm "Tacinterp.tac_interp" (str
-    "Interpretation gives a non-tactic value") *)
-
-(*    match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
-      | VClosure tac -> (tac g)
-      | VFTactic (largs,f) -> (f largs g) 
-      | VRTactic res -> res
-      | _ ->
-        errorlabstrm "Tacinterp.tac_interp" (str
-          "Interpretation gives a non-tactic value")*)
-
 (* Interprets a primitive tactic *)
-and interp_atomic ist = function
+and interp_atomic ist gl = function
   (* Basic tactics *)
   | TacIntroPattern l ->
       Elim.h_intro_patterns (List.map (interp_intro_pattern ist) l)
-  | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp)
+  | TacIntrosUntil hyp ->
+      h_intros_until (interp_quantified_hypothesis ist gl hyp)
   | TacIntroMove (ido,ido') ->
-      h_intro_move (option_app (ident_interp ist) ido)
-      (option_app (fun x -> ident_interp ist (snd x)) ido')
+      h_intro_move (option_app (eval_ident ist) ido)
+      (option_app (fun x -> eval_variable ist gl x) ido')
   | TacAssumption -> h_assumption
-  | TacExact c -> h_exact (cast_constr_interp ist c)
-  | TacApply cb -> h_apply (interp_constr_with_bindings ist cb)
+  | TacExact c -> h_exact (cast_constr_interp ist gl c)
+  | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
   | TacElim (cb,cbo) ->
-      h_elim (interp_constr_with_bindings ist cb)
-                (option_app (interp_constr_with_bindings ist) cbo)
-  | TacElimType c -> h_elim_type (constr_interp ist c)
-  | TacCase cb -> h_case (interp_constr_with_bindings ist cb)
-  | TacCaseType c -> h_case_type (constr_interp ist c)
-  | TacFix (idopt,n) -> h_fix (id_opt_interp ist idopt) n
+      h_elim (interp_constr_with_bindings ist gl cb)
+                (option_app (interp_constr_with_bindings ist gl) cbo)
+  | TacElimType c -> h_elim_type (pf_constr_interp ist gl c)
+  | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
+  | TacCaseType c -> h_case_type (pf_constr_interp ist gl c)
+  | TacFix (idopt,n) -> h_fix (eval_opt_ident ist idopt) n
   | TacMutualFix (id,n,l) ->
-      let f (id,n,c) = (ident_interp ist id,n,constr_interp ist c) in
-      h_mutual_fix (ident_interp ist id) n (List.map f l)
-  | TacCofix idopt -> h_cofix (id_opt_interp ist idopt)
+      let f (id,n,c) = (eval_ident ist id,n,pf_constr_interp ist gl c) in
+      h_mutual_fix (eval_ident ist id) n (List.map f l)
+  | TacCofix idopt -> h_cofix (eval_opt_ident ist idopt)
   | TacMutualCofix (id,l) ->
-      let f (id,c) = (ident_interp ist id,constr_interp ist c) in
-      h_mutual_cofix (ident_interp ist id) (List.map f l)
-  | TacCut c -> h_cut (constr_interp ist c)
-  | TacTrueCut (ido,c) -> h_true_cut (id_opt_interp ist ido) (constr_interp ist c)
-  | TacForward (b,na,c) -> h_forward b (name_interp ist na) (constr_interp ist c)
-  | TacGeneralize cl -> h_generalize (List.map (constr_interp ist) cl)
-  | TacGeneralizeDep c -> h_generalize_dep (constr_interp ist c)
+      let f (id,c) = (eval_ident ist id,pf_constr_interp ist gl c) in
+      h_mutual_cofix (eval_ident ist id) (List.map f l)
+  | TacCut c -> h_cut (pf_constr_interp ist gl c)
+  | TacTrueCut (ido,c) -> h_true_cut (eval_opt_ident ist ido) (pf_constr_interp ist gl c)
+  | TacForward (b,na,c) -> h_forward b (eval_name ist na) (pf_constr_interp ist gl c)
+  | TacGeneralize cl -> h_generalize (List.map (pf_constr_interp ist gl) cl)
+  | TacGeneralizeDep c -> h_generalize_dep (pf_constr_interp ist gl c)
   | TacLetTac (id,c,clp) ->
-      let clp = check_clause_pattern ist clp in
-      h_let_tac (ident_interp ist id) (constr_interp ist c) clp
-  | TacInstantiate (n,c) -> h_instantiate n (constr_interp ist c)
+      let clp = check_clause_pattern ist gl clp in
+      h_let_tac (eval_ident ist id) (pf_constr_interp ist gl c) clp
+  | TacInstantiate (n,c) -> h_instantiate n (pf_constr_interp ist gl c)
 
   (* Automation tactics *)
   | TacTrivial l -> Auto.h_trivial l
   | TacAuto (n, l) -> Auto.h_auto n l
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
-  | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (hyp_interp ist id)
+  | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (hyp_interp 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 (n,p)
 
   (* Derived basic tactics *)
-  | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist h)
+  | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist gl h)
   | TacNewInduction (c,cbo,ids) ->
-      h_new_induction (interp_induction_arg ist c)
-        (option_app (interp_constr_with_bindings ist) cbo)
-        (List.map (List.map (ident_interp ist)) ids)
-  | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist h)
+      h_new_induction (interp_induction_arg ist gl c)
+        (option_app (interp_constr_with_bindings ist gl) cbo)
+        (List.map (List.map (eval_ident ist)) ids)
+  | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist gl h)
   | TacNewDestruct (c,cbo,ids) -> 
-      h_new_destruct (interp_induction_arg ist c)
-        (option_app (interp_constr_with_bindings ist) cbo)
-        (List.map (List.map (ident_interp ist)) ids)
+      h_new_destruct (interp_induction_arg ist gl c)
+        (option_app (interp_constr_with_bindings ist gl) cbo)
+        (List.map (List.map (eval_ident ist)) ids)
   | TacDoubleInduction (h1,h2) ->
-      let h1 = interp_quantified_hypothesis ist h1 in
-      let h2 = interp_quantified_hypothesis ist h2 in
+      let h1 = interp_quantified_hypothesis ist gl h1 in
+      let h2 = interp_quantified_hypothesis ist gl h2 in
       Elim.h_double_induction h1 h2
-  | TacDecomposeAnd c -> Elim.h_decompose_and (constr_interp ist c)
-  | TacDecomposeOr c -> Elim.h_decompose_or (constr_interp ist c)
+  | TacDecomposeAnd c -> Elim.h_decompose_and (pf_constr_interp ist gl c)
+  | TacDecomposeOr c -> Elim.h_decompose_or (pf_constr_interp ist gl c)
   | TacDecompose (l,c) ->
-      let l = List.map (interp_inductive_or_metanum ist) l in
-      Elim.h_decompose l (constr_interp ist c)
-  | TacSpecialize (n,l) -> h_specialize n (interp_constr_with_bindings ist l)
-  | TacLApply c -> h_lapply (constr_interp ist c)
+      let l = List.map (interp_inductive_or_metanum ist gl) l in
+      Elim.h_decompose l (pf_constr_interp ist gl c)
+  | TacSpecialize (n,l) -> h_specialize n (interp_constr_with_bindings ist gl l)
+  | TacLApply c -> h_lapply (pf_constr_interp ist gl c)
 
   (* Context management *)
-  | TacClear l -> h_clear (List.map (hyp_or_metanum_interp ist) l)
-  | TacClearBody l -> h_clear_body (List.map (hyp_or_metanum_interp ist) l)
+  | TacClear l -> h_clear (List.map (hyp_or_metanum_interp ist gl) l)
+  | TacClearBody l -> h_clear_body (List.map (hyp_or_metanum_interp ist gl) l)
   | TacMove (dep,id1,id2) ->
-      h_move dep (hyp_interp ist id1) (hyp_interp ist id2)
+      h_move dep (hyp_interp ist gl id1) (hyp_interp ist gl id2)
   | TacRename (id1,id2) ->
-      h_rename (hyp_interp ist id1) (hyp_interp ist id2)
+      h_rename (hyp_interp ist gl id1) (eval_ident ist (snd id2))
 
   (* Constructors *)
-  | TacLeft bl -> h_left (bindings_interp ist bl)
-  | TacRight bl -> h_right (bindings_interp ist bl)
-  | TacSplit bl -> h_split (bindings_interp ist bl)
+  | TacLeft bl -> h_left (bindings_interp ist gl bl)
+  | TacRight bl -> h_right (bindings_interp ist gl bl)
+  | TacSplit bl -> h_split (bindings_interp ist gl bl)
   | TacAnyConstructor t ->
       abstract_tactic (TacAnyConstructor t)
         (Tactics.any_constructor (option_app (tactic_interp ist) t))
   | TacConstructor (n,bl) ->
-      h_constructor (skip_metaid n) (bindings_interp ist bl)
+      h_constructor (skip_metaid n) (bindings_interp ist gl bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      h_reduce (redexp_interp ist r) (List.map (interp_hyp_location ist) cl)
+      h_reduce (pf_redexp_interp ist gl r) (List.map (interp_hyp_location ist gl) cl)
   | TacChange (occl,c,cl) ->
-      h_change (option_app (pattern_interp ist) occl)
-        (constr_interp ist c) (List.map (interp_hyp_location ist) cl)
+      h_change (option_app (pf_pattern_interp ist gl) occl)
+        (pf_constr_interp ist gl c) (List.map (interp_hyp_location ist gl) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
   | TacSymmetry -> h_symmetry
-  | TacTransitivity c -> h_transitivity (constr_interp ist c)
+  | TacTransitivity c -> h_transitivity (pf_constr_interp ist gl c)
 
   (* For extensions *)
-  | TacExtend (loc,opn,l) -> vernac_tactic (opn,List.map (genarg_interp ist) l)
-  | TacAlias (_,l,body) ->
-      let f x = match genarg_tag x with
-  | IdentArgType -> VIdentifier (ident_interp ist (out_gen rawwit_ident x))
-  | RefArgType -> VConstr (constr_of_reference (reference_interp ist (out_gen rawwit_ref x)))
-  | ConstrArgType -> VConstr (constr_interp ist (out_gen rawwit_constr x))
-  | ConstrMayEvalArgType ->
-      VConstr (constr_interp_may_eval ist (out_gen rawwit_constr_may_eval x))
-  | _ -> failwith "This generic type is not supported in alias" in
-
-      tactic_of_value (val_interp { ist with lfun=(List.map (fun (x,c) -> (x,f c)) l)@ist.lfun } body)
+  | TacExtend (loc,opn,l) ->
+      fun gl -> vernac_tactic (opn,List.map (genarg_interp ist gl) l) gl
+  | TacAlias (_,l,body) -> fun gl ->
+    let f x = match genarg_tag x with
+    | IdentArgType -> 
+	let id = out_gen rawwit_ident x in
+	(try VConstr (mkVar (eval_variable ist gl (dummy_loc,id)))
+	 with Not_found -> VIdentifier id)
+    | RefArgType -> VConstr (constr_of_reference (pf_reference_interp ist gl (out_gen rawwit_ref x)))
+    | ConstrArgType -> VConstr (pf_constr_interp ist gl (out_gen rawwit_constr x))
+    | ConstrMayEvalArgType ->
+      VConstr (constr_interp_may_eval ist gl (out_gen rawwit_constr_may_eval x))
+    | _ -> failwith "This generic type is not supported in alias"
+    in
+    let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
+    tactic_of_value (val_interp { ist with lfun=lfun } gl body) gl
 
-let _ = forward_vcontext_interp := vcontext_interp
- 
 (* Interprets tactic arguments *)
 let interp_tacarg sign ast = (*unvarg*) (val_interp sign ast)
 
 (* Initial call for interpretation *)
-let interp = fun ast -> tac_interp [] [] !debug ast
+let tac_interp lfun lmatch debug t = 
+  tactic_interp { lfun=lfun; lmatch=lmatch; debug=debug } t
+
+let interp = tac_interp [] [] (get_debug())
 
 (* Hides interpretation for pretty-print *)
-let hide_interp t ot =  
+let hide_interp t ot gl =
+  let te = glob_tactic ([],[],project gl,pf_env gl) t in
   match ot with 
-  | None -> abstract_tactic_expr (TacArg (Tacexp t)) (interp t)
-  | Some t' -> abstract_tactic_expr (TacArg (Tacexp t)) (tclTHEN (interp t) t')
+  | None -> abstract_tactic_expr (TacArg (Tacexp t)) (interp t) gl
+  | Some t' ->
+      abstract_tactic_expr (TacArg (Tacexp t)) (tclTHEN (interp t) t') gl
 
 (* For bad tactic calls *)
 let bad_tactic_args s =
@@ -1708,12 +1587,7 @@ let bad_tactic_args s =
 (* Declaration of the TAC-DEFINITION object *)
 let add (sp,td) = mactab := Gmap.add sp td !mactab
 
-let register_tacdef (sp,td) =
-  let ve = val_interp
-    {evc=Evd.empty;env=Global.env ();lfun=[];
-    lmatch=[]; goalopt=None; debug=get_debug ()}
-    td in
-  sp,ve
+let register_tacdef (sp,td) = sp,td
 
 let cache_md (_,defs) =
   (* Needs a rollback if something goes wrong *)
@@ -1735,19 +1609,18 @@ let make_absolute_name (loc,id) =
        ++ pr_sp sp);
   sp
 
-let add_tacdef tacl =
+let add_tacdef isrec tacl =
   let lfun = List.map (fun ((loc,id),_) -> id) tacl in
+  let ist = ((if isrec then lfun else []), [], Evd.empty, Global.env()) in
   let tacl = List.map (fun (id,tac) -> (make_absolute_name id,tac)) tacl in
-  List.iter (fun (_,def) -> let _ = glob_tactic (lfun,[]) def in ()) tacl;
+  let tacl = List.map (fun (id,def) -> (id,glob_tactic ist def)) tacl in
   let _ = Lib.add_leaf (List.hd lfun) (inMD tacl) in
   List.iter
     (fun id -> Options.if_verbose msgnl (pr_id id ++ str " is defined")) lfun
 
-let interp_redexp env evc r =
-  let ist =
-    { evc=evc; env=env; lfun=[]; lmatch=[]; goalopt=None; debug=get_debug ()}
-  in
-  redexp_interp ist r
+let interp_redexp env evc r = 
+  let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in
+  redexp_interp ist evc env r
 
 let _ = Auto.set_extern_interp (fun l -> tac_interp [] l (get_debug()))
 let _ = Dhyp.set_extern_interp interp
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c22ce9829c..9d63f33ef4 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -23,12 +23,8 @@ open Topconstr
 
 (* Values for interpretation *)
 type value =
-  | VClosure of interp_sign * raw_tactic_expr
   | VTactic of tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
-  | VFTactic of value list * (value list->tactic)
   | VRTactic of (goal list sigma * validation)
-  | VContext of interp_sign * direction_flag
-      * (pattern_expr,raw_tactic_expr) match_rule list
   | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
   | VVoid
   | VInteger of int
@@ -39,21 +35,18 @@ type value =
 
 (* Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
-  { evc : Evd.evar_map;
-    env : Environ.env;
-    lfun : (identifier * value) list;
+  { lfun : (identifier * value) list;
     lmatch : (int * constr) list;
-    goalopt : goal sigma option;
     debug : debug_info }
 
 (* Gives the identifier corresponding to an Identifier [tactic_arg] *)
-val id_of_Identifier : value -> identifier
+val id_of_Identifier : Environ.env -> value -> identifier
 
 (* Gives the constr corresponding to a Constr [value] *)
-val constr_of_VConstr : value -> constr
+val constr_of_VConstr : Environ.env -> value -> constr
 
 (* Transforms an id into a constr if possible *)
-val constr_of_id : interp_sign -> identifier -> constr
+val constr_of_id : Environ.env -> identifier -> constr
 
 (* To embed several objects in Coqast.t *)
 val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
@@ -70,18 +63,19 @@ val set_debug : debug_info -> unit
 val get_debug : unit -> debug_info
 
 (* Adds a definition for tactics in the table *)
-val add_tacdef : (identifier Util.located * raw_tactic_expr) list -> unit
+val add_tacdef :
+  bool -> (identifier Util.located * raw_tactic_expr) list -> unit
 
 (* Adds an interpretation function for extra generic arguments *)
 val add_genarg_interp :
   string ->
-    (interp_sign -> raw_generic_argument -> closed_generic_argument) -> unit
+    (interp_sign -> goal sigma -> raw_generic_argument -> closed_generic_argument) -> unit
 
 val genarg_interp :
-  interp_sign -> raw_generic_argument -> closed_generic_argument
+  interp_sign -> goal sigma -> raw_generic_argument -> closed_generic_argument
 
 (* Interprets any expression *)
-val val_interp : interp_sign -> raw_tactic_expr -> value
+val val_interp : interp_sign -> goal sigma -> raw_tactic_expr -> value
 
 (*
 (* Interprets tactic arguments *)
@@ -97,7 +91,7 @@ val tac_interp : (identifier * value) list -> (int * constr) list ->
                  debug_info -> raw_tactic_expr -> tactic
 
 (* Interprets constr expressions *)
-val constr_interp : interp_sign -> constr_expr -> constr
+val constr_interp : interp_sign -> Evd.evar_map -> Environ.env -> constr_expr -> constr
 
 (* Initial call for interpretation *)
 val interp : raw_tactic_expr -> tactic