Transparent

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

4 files changed, 284 insertions, 304 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b1cf3764e5..1dfc559732 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -177,7 +177,9 @@ let cook_proof () =
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in
   (ident,
-   ({ const_entry_body = pfterm; const_entry_type = Some concl },
+   ({ const_entry_body = pfterm;
+      const_entry_type = Some concl;
+      const_entry_opaque = true },
     strength))
 
 (*********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 3ca4ea6543..0ea59eea27 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -89,7 +89,7 @@ val resume_proof : identifier -> unit
 
 val suspend_proof : unit -> unit
 
-(*s [cook_proof ()] turns the current proof (assumed completed)
+(*s [cook_proof opacity] turns the current proof (assumed completed)
     into a constant with its name and strength; it fails if there is
     no current proof of if it is not completed *)
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 846344210c..098c2568e0 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -48,9 +48,14 @@ type value =
   | VRec of value ref
 
 (* Signature for interpretation: val_interp and interpretation functions *)
+
 and interp_sign =
-  enamed_declarations * Environ.env * (identifier * value) list *
-    (int * constr) list * goal sigma option * debug_info
+  { evc : enamed_declarations;
+    env : Environ.env;
+    lfun : (identifier * value) list;
+    lmatch : (int * constr) list;
+    goalopt : goal sigma option;
+    debug : debug_info }
 
 (* For tactic_of_value *)
 exception NotTactic
@@ -132,6 +137,14 @@ let rec constr_list goalopt = function
   | _::tl -> constr_list goalopt tl
   | [] -> []
 
+let interp_constr ist c ocl =
+  interp_constr_gen ist.evc ist.env
+    (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl
+
+let interp_openconstr ist c ocl =
+  interp_openconstr_gen ist.evc ist.env
+    (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl
+
 (* For user tactics *)
 let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t),
      (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml"
@@ -150,13 +163,13 @@ let r_goalopt = ref None
 let r_debug   = ref DebugOn
 
 (* Updates the references with the current environment *)
-let env_update (evc,env,lfun,lmatch,goalopt,debug) =
-  r_evc     := evc;
-  r_env     := env;
-  r_lfun    := lfun;
-  r_lmatch  := lmatch;
-  r_goalopt := goalopt;
-  r_debug   := debug
+let env_update ist =
+  r_evc     := ist.evc;
+  r_env     := ist.env;
+  r_lfun    := ist.lfun;
+  r_lmatch  := ist.lmatch;
+  r_goalopt := ist.goalopt;
+  r_debug   := ist.debug
 
 (* Table of interpretation functions *)
 let interp_tab =
@@ -192,19 +205,22 @@ let glob_const_nvar loc env qid =
       | [],id ->
 	  (* lookup_value may raise Not_found *)
 	  (match Environ.lookup_named_value id env with
-	     | Some _ -> EvalVarRef id
+	     | Some _ ->
+                 let v = EvalVarRef id in
+                 if Opaque.is_evaluable env v then v
+                 else error ("variable "^(string_of_id id)^" is opaque")
 	     | None -> error ((string_of_id id)^
 			      " does not denote an evaluable constant"))
       | _ -> raise Not_found
   with Not_found ->
   try
-    match Nametab.locate qid with
-      | ConstRef sp when Environ.evaluable_constant (Global.env ()) sp ->
-	  EvalConstRef sp
-      | VarRef sp when
-	  Environ.evaluable_named_decl (Global.env ()) (basename sp) ->
-	  EvalVarRef (basename sp)
+    let ev = (match Nametab.locate qid with
+      | ConstRef sp -> EvalConstRef sp
+      | VarRef sp -> EvalVarRef (basename sp)
       | _ -> error ((Nametab.string_of_qualid qid) ^
+		    " does not denote an evaluable constant")) in
+    if Opaque.is_evaluable env ev then ev
+    else error ((Nametab.string_of_qualid qid) ^
 		    " does not denote an evaluable constant")
   with Not_found ->
     Nametab.error_global_not_found_loc loc qid
@@ -447,8 +463,9 @@ let set_debug pos = debug := pos
 (* Gives the state of debug *)
 let get_debug () = !debug
 
+
 (* Interprets any expression *)
-let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
+let rec val_interp ist ast =
 
 (* mSGNL [<print_ast ast>]; *)
 (* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *)
@@ -456,137 +473,119 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
   let value_interp debug =
   match ast with
     | Node(_,"APP",l) ->
-      let fv = val_interp (evc,env,lfun,lmatch,goalopt,debug) (List.hd l)
-      and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt,debug))
-        (List.tl l) in
-      app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast
-    | Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1)
-    | Node(_,"REC",l) ->
-      rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast l
+        let fv = val_interp ist (List.hd l)
+        and largs = List.map (val_interp ist) (List.tl l) in
+      app_interp ist fv largs ast
+    | Node(_,"FUN",l) -> VFun (ist.lfun,read_fun (List.hd l),List.nth l 1)
+    | Node(_,"REC",l) -> rec_interp ist ast l
     | Node(_,"LET",[Node(_,"LETDECL",l);u]) ->
-      let addlfun=letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast l in
-        val_interp (evc,env,addlfun@lfun,lmatch,goalopt,debug) u
+        let addlfun=letin_interp ist ast l in
+        val_interp { ist with lfun=addlfun@ist.lfun } u
     | Node(_,"LETCUT",[Node(_,"LETDECL",l)]) ->
-      VTactic (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast l)
-    | Node(_,"MATCHCONTEXT",lmr) ->
-      match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr
-    | Node(_,"MATCH",lmr) ->
-      match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr
+        VTactic (letcut_interp ist ast l)
+    | Node(_,"MATCHCONTEXT",lmr) -> match_context_interp ist ast lmr
+    | Node(_,"MATCH",lmr) -> match_interp ist ast lmr
     | Node(_,"IDTAC",[]) -> VTactic tclIDTAC
     | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0)
     | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n))
     | Node(_,"PROGRESS",[tac]) ->
-      VTactic (tclPROGRESS (tac_interp lfun lmatch debug tac))
+        VTactic (tclPROGRESS (tactic_interp ist tac))
     | Node(_,"TACTICLIST",l) ->
-      VTactic (interp_semi_list tclIDTAC lfun lmatch debug l)
+        VTactic (interp_semi_list tclIDTAC ist.lfun ist.lmatch ist.debug l)
     | Node(_,"DO",[n;tac]) ->
-      VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch debug tac))
-    | Node(_,"TRY",[tac]) ->
-      VTactic (tclTRY (tac_interp lfun lmatch debug tac))
-    | Node(_,"INFO",[tac]) ->
-      VTactic (tclINFO (tac_interp lfun lmatch debug tac))
-    | Node(_,"REPEAT",[tac]) ->
-      VTactic (tclREPEAT (tac_interp lfun lmatch debug tac))
+        VTactic (tclDO (num_of_ast n) (tactic_interp ist tac))
+    | Node(_,"TRY",[tac]) -> VTactic (tclTRY (tactic_interp ist tac))
+    | Node(_,"INFO",[tac]) -> VTactic (tclINFO (tactic_interp ist tac))
+    | Node(_,"REPEAT",[tac]) -> VTactic (tclREPEAT (tactic_interp ist tac))
     | Node(_,"ORELSE",[tac1;tac2]) ->
-      VTactic (tclORELSE (tac_interp lfun lmatch debug tac1)
-        (tac_interp lfun lmatch debug tac2))
-    | Node(_,"FIRST",l) ->
-      VTactic (tclFIRST (List.map (tac_interp lfun lmatch debug) l))
+        VTactic (tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2))
+    | Node(_,"FIRST",l) -> VTactic (tclFIRST (List.map (tactic_interp ist) l))
     | Node(_,"TCLSOLVE",l) ->
-      VTactic (tclSOLVE (List.map (tac_interp lfun lmatch debug) l))
+        VTactic (tclSOLVE (List.map (tactic_interp ist) l))
     | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
-      val_interp (evc,env,lfun,lmatch,goalopt,debug)
-        (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
+        val_interp ist
+          (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
     | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) ->
-      VFTactic ([],(interp_atomic opn))
+        VFTactic ([],(interp_atomic opn))
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
-      (try (unrec (List.assoc s lfun))
-       with | Not_found ->
-         (try (vcontext_interp goalopt (lookup s))
-          with | Not_found -> VArg (Identifier s)))
+        (try (unrec (List.assoc s ist.lfun))
+        with | Not_found ->
+                 (try (vcontext_interp ist.goalopt (lookup s))
+                 with | Not_found -> VArg (Identifier s)))
     | Node(_,"QUALIDARG",[Nvar(_,s)]) ->
-      (try (make_qid (unrec (List.assoc s lfun)))
-       with | Not_found ->
-         VArg (Qualid (qid_interp (evc,env,lfun,lmatch,goalopt,debug) ast)))
+        (try (make_qid (unrec (List.assoc s ist.lfun)))
+        with | Not_found ->
+                 VArg (Qualid (qid_interp ist ast)))
     | Node(_,"QUALIDARG",_) | Node(_,"QUALIDMETA",_) ->
-      VArg (Qualid (qid_interp (evc,env,lfun,lmatch,goalopt,debug) ast))
+        VArg (Qualid (qid_interp ist ast))
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
-    | Node(_,"COMMAND",[c]) ->
-      com_interp (evc,env,lfun,lmatch,goalopt,debug) c
-    | Node(_,"CASTEDCOMMAND",[c]) ->
-      cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) c
-    | Node(_,"CASTEDOPENCOMMAND",[c]) ->
-      cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) c
+    | Node(_,"COMMAND",[c]) -> com_interp ist c
+    | Node(_,"CASTEDCOMMAND",[c]) -> cast_com_interp ist c
+    | Node(_,"CASTEDOPENCOMMAND",[c]) -> cast_opencom_interp ist c
     | Node(_,"BINDINGS",astl) ->
-      VArg (Cbindings (List.map (bind_interp
-        (evc,env,lfun,lmatch,goalopt,debug)) astl))
+        VArg (Cbindings (List.map (bind_interp ist) astl))
     | Node(_,"REDEXP",[Node(_,redname,args)]) ->
-      VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug)
-        (redname,args)))
+        VArg (Redexp (redexp_of_ast ist (redname,args)))
     | Node(_,"CLAUSE",cl) ->
-      VArg (Clause (List.map (clause_interp 
-        (evc,env,lfun,lmatch,goalopt,debug)) cl))
+        VArg (Clause (List.map (clause_interp ist) cl))
     | Node(_,"TACTIC",[ast]) ->
-      VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
+        VArg (Tac ((tactic_interp ist ast),ast))
 (*Remains to treat*)
     | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
-      VArg ((Fixexp (s,n,c)))
+        VArg ((Fixexp (s,n,c)))
     | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
-      VArg ((Cofixexp (s,c)))
+        VArg ((Cofixexp (s,c)))
 (*End of Remains to treat*)
     | Node(_,"INTROPATTERN", [ast]) ->
-      VArg ((Intropattern (cvt_intro_pattern
-        (evc,env,lfun,lmatch,goalopt,debug) ast)))
+        VArg ((Intropattern (cvt_intro_pattern ist ast)))
     | Node(_,"LETPATTERNS",astl) ->
-      VArg (Letpatterns (List.fold_left (cvt_letpattern
-        (evc,env,lfun,lmatch,goalopt,debug)) (None,[]) astl))
+        VArg (Letpatterns (List.fold_left (cvt_letpattern ist) (None,[]) astl))
     | Node(loc,s,l) ->
-      (try
-         ((look_for_interp s) (evc,env,lfun,lmatch,goalopt,debug) ast)
-       with
+        (try
+          ((look_for_interp s) ist ast)
+        with
            Not_found ->
-             val_interp (evc,env,lfun,lmatch,goalopt,debug)
-               (Node(dummy_loc,"APPTACTIC",[ast])))
+             val_interp ist (Node(dummy_loc,"APPTACTIC",[ast])))
     | Dynamic(_,t) -> 
-      env_update (evc,env,lfun,lmatch,goalopt,debug);
-      let f = (ocamlOut t) in
-      Obj.magic (val_interp (evc,env,lfun,lmatch,goalopt,debug) (f ()))
+        env_update ist;
+        let f = (ocamlOut t) in
+        Obj.magic (val_interp ist (f ()))
     | _ ->
-      anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR
-        "Unrecognizable ast: "; print_ast ast>]) in
-  if debug = DebugOn then
-    match debug_prompt goalopt ast with
+        anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",
+                     [<'sTR "Unrecognizable ast: "; print_ast ast>]) in
+  if ist.debug = DebugOn then
+    match debug_prompt ist.goalopt ast with
     | Exit -> VTactic tclIDTAC
     | v -> value_interp v
   else
     value_interp debug
 
 (* Interprets an application node *)
-and app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast =
+and app_interp ist fv largs ast =
   match fv with
     | VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f)
     | VFun(olfun,var,body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
         if lval=[] then
-          val_interp (evc,env,(olfun@newlfun),lmatch,goalopt,debug) body
+          val_interp { ist with lfun=olfun@newlfun } body
         else
-          app_interp (evc,env,lfun,lmatch,goalopt,debug) (val_interp (evc,env,
-            (olfun@newlfun),lmatch,goalopt,debug) body) lval ast
+          app_interp ist
+            (val_interp {ist with lfun=olfun@newlfun } body) lval ast
       else
         VFun(olfun@newlfun,lvar,body)
     | _ ->
-      user_err_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
-        "Illegal tactic application: "; print_ast ast>])
+      user_err_loc (Ast.loc ast, "Tacinterp.app_interp",
+                    [<'sTR"Illegal tactic application: "; print_ast ast>])
 
 (* Interprets recursive expressions *)
-and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
+and rec_interp ist ast = function
   | [Node(_,"RECCLAUSE",_)] as l ->
      let (name,var,body) = List.hd (read_rec_clauses l)
      and ve = ref VVoid in
-       let newve = VFun(lfun@[(name,VRec ve)],read_fun var,body) in
+       let newve = VFun(ist.lfun@[(name,VRec ve)],read_fun var,body) in
        begin
          ve:=newve;
          !ve
@@ -596,45 +595,40 @@ and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
     let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
     let lenv = List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l)
       lrc lref [] in
-    let lve = List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun
-      var,body))) lrc in
+    let lve = List.map (fun (name,var,body) ->
+                          (name,VFun(ist.lfun@lenv,read_fun var,body))) lrc in
     begin
       List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
-      val_interp (evc,env,(lfun@lve),lmatch,goalopt,debug) u
+      val_interp { ist with lfun=ist.lfun@lve } u
     end
   | _ ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR
-      "Rec not well formed: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",
+                 [<'sTR"Rec not well formed: "; print_ast ast>])
 
 (* Interprets the clauses of a Let *)
-and let_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
+and let_interp ist ast = function
   | [] -> []
   | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
-    (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t)::
-      (let_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+      (id,val_interp ist t)::(let_interp ist ast tl)
   | _ ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR
-      "Let not well formed: "; print_ast ast>])
+      anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",
+                   [<'sTR"Let not well formed: "; print_ast ast>])
 
 (* Interprets the clauses of a LetCutIn *)
-and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
+and letin_interp ist ast = function
   | [] -> []
   | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
-    (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t)::
-      (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+      (id,val_interp ist t):: (letin_interp ist ast tl)
   | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl ->
-    let typ =
-      constr_of_Constr (unvarg
-      (val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
-    and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce in
+    let typ = constr_of_Constr (unvarg (val_interp ist com))
+    and tac = val_interp ist tce in
     (match tac with
     | VArg (Constr csr) ->
-      (id,VArg (Constr (mkCast (csr,typ))))::
-      (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+      (id,VArg (Constr (mkCast (csr,typ))))::(letin_interp ist ast tl)
     | VArg (Identifier id) ->
       (try
-         (id,VArg (Constr (mkCast (constr_of_id id goalopt,typ))))::
-         (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+         (id,VArg (Constr (mkCast (constr_of_id id ist.goalopt,typ))))::
+         (letin_interp ist ast tl)
        with | Not_found ->
          errorlabstrm "Tacinterp.letin_interp"
          [< 'sTR "Term or tactic expected" >])
@@ -642,7 +636,7 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
       (try
          let t = tactic_of_value tac in
          let ndc =
-           (match goalopt with
+           (match ist.goalopt with
            | None -> Global.named_context ()
            | Some g -> pf_hyps g) in
          start_proof id NeverDischarge ndc typ;
@@ -650,8 +644,7 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
          let (_,({const_entry_body = pft; const_entry_type = _},_)) =
            cook_proof () in
          delete_proof id;
-         (id,VArg (Constr (mkCast (pft,typ))))::
-         (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+         (id,VArg (Constr (mkCast (pft,typ))))::(letin_interp ist ast tl)
        with | NotTactic ->
          delete_proof id;
          errorlabstrm "Tacinterp.letin_interp"
@@ -661,15 +654,13 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
     [<'sTR "LetIn not well formed: "; print_ast ast>])
 
 (* Interprets the clauses of a LetCut *)
-and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
+and letcut_interp ist ast = function
   | [] -> tclIDTAC
   | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl ->
-    let typ =
-      constr_of_Constr (unvarg
-      (val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
-    and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce
+    let typ = constr_of_Constr (unvarg (val_interp ist com))
+    and tac = val_interp ist tce
     and (ndc,ccl) =
-      match goalopt with
+      match ist.goalopt with
       |	None -> 
         errorlabstrm "Tacinterp.letcut_interp" [< 'sTR
         "Do not use Let for toplevel definitions, use Lemma, ... instead" >]
@@ -679,19 +670,20 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
       let cutt = interp_atomic "Cut" [Constr typ]
       and exat = interp_atomic "Exact" [Constr csr] in
       tclTHENS cutt [tclTHEN (introduction id)
-      (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat]
+      (letcut_interp ist ast tl);exat]
 
 (*      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 (evc,env,lfun,lmatch,goalopt,debug) ast tl))*)
+      (letcut_interp ist ast tl))*)
 
     | VArg (Identifier ir) ->
       (try
          let cutt = interp_atomic "Cut" [Constr typ]
-         and exat = interp_atomic "Exact" [Constr (constr_of_id ir goalopt)] in
+         and exat =
+           interp_atomic "Exact" [Constr (constr_of_id ir ist.goalopt)] in
          tclTHENS cutt [tclTHEN (introduction id)
-         (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat]
+         (letcut_interp ist ast tl);exat]
        with | Not_found ->
          errorlabstrm "Tacinterp.letin_interp"
          [< 'sTR "Term or tactic expected" >])
@@ -706,12 +698,12 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
          let cutt = interp_atomic "Cut" [Constr typ]
          and exat = interp_atomic "Exact" [Constr pft] in
          tclTHENS cutt [tclTHEN (introduction id)
-         (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat]
+         (letcut_interp ist ast 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 (evc,env,lfun,lmatch,goalopt,debug) ast tl))*)
+         (letcut_interp ist ast tl))*)
        with | NotTactic ->
          delete_proof id;
          errorlabstrm "Tacinterp.letcut_interp"
@@ -721,38 +713,40 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
       "LetCut not well formed: "; print_ast ast>])
 
 (* Interprets the Match Context expressions *)
-and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
+and match_context_interp ist ast lmr =
 (*  let goal =
     (match goalopt with
     | None ->
       errorlabstrm "Tacinterp.apply_match_context" [< 'sTR
         "No goal available" >]
     | Some g -> g) in*)
-  let rec apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal nocc (id,c)
+  let rec apply_goal_sub ist goal 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
-          (evc,env,lctxt@lfun,lgoal@lmatch,Some goal,debug)) mt goal
+        eval_with_fail
+          (val_interp
+            { ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch;
+                       goalopt=Some goal})
+          mt goal
       else
-        apply_hyps_context evc env (lctxt@lfun) lmatch goal debug mt lgoal
-          mhyps hyps
+        apply_hyps_context {ist with goalopt=Some goal} mt lgoal mhyps hyps
     with
     | (FailError _) as e -> raise e
     | NextOccurrence _ -> raise No_match
     | No_match | _ ->
-      apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal (nocc + 1) (id,c)
+      apply_goal_sub ist goal (nocc + 1) (id,c)
       csr mt mhyps hyps in
-  let rec apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal =
+  let rec apply_match_context ist goal =
     function
     | (All t)::tl ->
       (try
-         eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal,debug)) t
+         eval_with_fail (val_interp {ist with goalopt=Some goal }) t
            goal
        with No_match | _ ->
-         apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl)
+         apply_match_context ist goal tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
       let hyps = make_hyps (List.rev (pf_hyps goal))
       and concl = pf_concl goal in
@@ -761,23 +755,20 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
         (try
            (let lgoal = apply_matching mg concl in
             begin
-            db_matched_concl debug env concl;
+            db_matched_concl ist.debug ist.env concl;
             if mhyps = [] then
               eval_with_fail (val_interp
-                (evc,env,lfun,lgoal@lmatch,Some goal,debug)) mt goal
+                {ist with lmatch=lgoal@ist.lmatch; goalopt=Some goal}) mt goal
             else
-              apply_hyps_context evc env lfun lmatch goal debug mt lgoal mhyps
+              apply_hyps_context { ist with goalopt=Some goal} mt lgoal mhyps
                 hyps
             end)
-         with | No_match | _ ->
-           apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl)
+         with | No_match | _ -> apply_match_context ist goal tl)
       |	Subterm (id,mg) ->
         (try
-          apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal 0 (id,mg)
-          concl mt mhyps hyps
+          apply_goal_sub ist goal 0 (id,mg) concl mt mhyps hyps
          with
-        | No_match | _ ->
-          apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl))
+        | No_match | _ -> apply_match_context ist goal tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match_context" [<'sTR
         "No matching clauses for Match Context">] in
@@ -785,14 +776,15 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
     (fun goal ->
        let evc = project goal
        and env = pf_env goal in
-       apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal
-         (read_match_context_rule evc env (constr_list goalopt lfun) lmr)) in
+       apply_match_context ist goal
+         (read_match_context_rule ist.evc ist.env
+           (constr_list ist.goalopt ist.lfun) lmr)) in
 
-(*    (fun (evc,env,lfun,lmatch,goalopt,debug) goal ->
-     apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal
+(*    (fun ist goal ->
+     apply_match_context ist goal
      (read_match_context_rule evc env (constr_list goalopt lfun) lmr)) in*)
 
- (match goalopt with
+ (match ist.goalopt with
     | None -> VContext app_wo_goal
     | Some g -> app_wo_goal g)
 
@@ -800,43 +792,44 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
     (constr_list goalopt lfun) lmr)*)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context evc env lfun_glob lmatch_glob goal debug mt lgmatch
-  mhyps hyps =
-  let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
-    lmatch mhyps lhyps_mhyp lhyps_rest noccopt =
+and apply_hyps_context ist mt lgmatch mhyps hyps =
+  let rec apply_hyps_context_rec ist 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 lmatch hd lhyps_mhyp noccopt in
         begin
-        db_matched_hyp debug env hyp_match;
+        db_matched_hyp ist.debug ist.env hyp_match;
         (try
         if tl = [] then
-            eval_with_fail (val_interp (evc,env,(lfun@lid@lc@lfun_glob),
-              (lmatch@lm@lmatch_glob),Some goal,debug)) mt goal
+            eval_with_fail
+              (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
+                                    lmatch=lmatch@lm@ist.lmatch;
+                                    goalopt=Some goal})
+              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 evc env lfun_glob lmatch_glob goal mt
+          apply_hyps_context_rec ist mt
             (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
          with
         | (FailError _) as e -> raise e
         | _ ->
           (match noccopt with
           | None ->
-            apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
+            apply_hyps_context_rec ist mt lfun
               lmatch mhyps newlhyps lhyps_rest None
           | Some nocc ->
-            apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
-              lmatch mhyps (hyp_match::newlhyps) lhyps_rest (Some (nocc +
-              1))))
+            apply_hyps_context_rec ist 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 evc env lfun_glob lmatch_glob goal mt [] lgmatch mhyps
-    hyps hyps None
+  apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
 
 (* Interprets a VContext value *)
 and vcontext_interp goalopt = function
@@ -847,78 +840,81 @@ and vcontext_interp goalopt = function
   | v -> v
 
 (* Interprets the Match expressions *)
-and match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
-  let rec apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) nocc (id,c) csr
+and match_interp ist ast lmr =
+  let rec apply_sub_match ist nocc (id,c) csr
     mt =
-    match goalopt with
+    match ist.goalopt with
     | None ->
       (try 
         let (lm,ctxt) = sub_match nocc c csr in
         let lctxt = give_context ctxt id in
-        val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug) mt
+        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
-          (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug)) mt g
+        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
-       | _ ->
-         apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) (nocc + 1) (id,c)
-           csr mt)
+       | _ -> apply_sub_match ist (nocc + 1) (id,c) csr mt)
   in
-  let rec apply_match (evc,env,lfun,lmatch,goalopt,debug) csr = function
+  let rec apply_match ist csr = function
     | (All t)::_ ->
-      (match goalopt with
+      (match ist.goalopt with
         | None ->
-          (try val_interp (evc,env,lfun,lmatch,goalopt,debug) t
-           with | No_match | _ ->
-             apply_match (evc,env,lfun,lmatch,goalopt,debug) csr [])
+          (try val_interp ist t
+           with | No_match | _ -> apply_match ist csr [])
         | Some g ->
           (try
-            eval_with_fail (val_interp (evc,env,lfun,lmatch,goalopt,debug)) t g
+            eval_with_fail (val_interp ist) t g
            with
            | (FailError _) as e -> raise e
-           | _ -> apply_match (evc,env,lfun,lmatch,goalopt,debug) csr []))
+           | _ -> apply_match ist csr []))
     | (Pat ([],mp,mt))::tl ->
       (match mp with
       |	Term c ->
-        (match goalopt with
+        (match ist.goalopt with
         | None ->
           (try
              val_interp
-               (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt,debug) mt
+               { ist with lmatch=(apply_matching c csr)@ist.lmatch } mt
            with | No_match | _ ->
-             apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl)
+             apply_match ist csr tl)
         | Some g ->
           (try
             eval_with_fail (val_interp
-              (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt,debug)) mt g
+              { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g
            with
            | (FailError _) as e -> raise e
-           | _ -> apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl))
+           | _ -> apply_match ist csr tl))
       |	Subterm (id,c) ->
         (try
-           apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) 0 (id,c) csr mt
+           apply_sub_match ist 0 (id,c) csr mt
          with | No_match ->
-           apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl))
+           apply_match ist csr tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match" [<'sTR
         "No matching clauses for Match">] in
   let csr =
-    constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug)
-      (List.hd lmr)))
-  and ilr = read_match_rule evc env (constr_list goalopt lfun) (List.tl lmr) in
-  apply_match (evc,env,lfun,lmatch,goalopt,debug) csr ilr
+    constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
+  and ilr = read_match_rule
+    ist.evc ist.env (constr_list ist.goalopt ist.lfun) (List.tl lmr) in
+  apply_match ist csr ilr
+
+and tactic_interp ist ast 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
-  try tactic_of_value (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) g
+  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
   with | NotTactic ->
     errorlabstrm "Tacinterp.tac_interp" [<'sTR
     "Interpretation gives a non-tactic value">]
@@ -945,60 +941,54 @@ and interp_semi_list acc lfun lmatch debug = function
   | [] -> acc
 
 (* Interprets bindings for tactics *)
-and bind_interp (evc,env,lfun,lmatch,goalopt,debug) = function
+and bind_interp ist = function
   | Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) ->
     (NoDep n,constr_of_Constr (unvarg (val_interp
-      (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[c])))))
+      ist (Node(loc,"COMMAND",[c])))))
   | Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> 
     (Dep (id_of_Identifier (unvarg (val_interp
-      (evc,env,lfun,lmatch,goalopt,debug)
+      ist
       (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp
-      (evc,env,lfun,lmatch,goalopt,debug) (Node(loc1,"COMMAND",[c])))))
+      ist (Node(loc1,"COMMAND",[c])))))
   | Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) ->
     (Com,constr_of_Constr (unvarg
-      (val_interp (evc,env,lfun,lmatch,goalopt,debug)
+      (val_interp ist
       (Node(loc,"COMMAND",[c])))))
   | x ->
     errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding";
       print_ast x>]
 
 (* Interprets a COMMAND expression (in case of failure, returns Command) *)
-and com_interp (evc,env,lfun,lmatch,goalopt,debug) = function
+and com_interp ist = function
   | Node(_,"EVAL",[c;rtc]) ->
-    let redexp = unredexp (unvarg (val_interp
-      (evc,env,lfun,lmatch,goalopt,debug) rtc)) in
-    VArg (Constr ((reduction_of_redexp redexp) env evc
-		    (interp_constr_gen evc env (constr_list goalopt lfun)
-		       lmatch c None)))
+    let redexp = unredexp (unvarg (val_interp ist rtc)) in
+    VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc
+		    (interp_constr ist c None)))
   | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
     (try
-      let ic =
-	interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None
-      and ctxt = constr_of_Constr_context (unvarg (List.assoc s lfun)) in
+      let ic = interp_constr ist c None
+      and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in
       VArg (Constr (subst_meta [-1,ic] ctxt))
      with
     | Not_found ->
       errorlabstrm "com_interp" [<'sTR "Unbound context identifier";
         print_ast ast>])
-  | c ->
-    VArg (Constr
-      (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None))
+  | c -> VArg (Constr (interp_constr ist c None))
 
 (* Interprets a CASTEDCOMMAND expression *)
-and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com =
-  match goalopt with
+and cast_com_interp ist com =
+  match ist.goalopt with
   | Some gl ->
     (match com with
     | Node(_,"EVAL",[c;rtc]) ->
       let redexp = unredexp (unvarg (val_interp
-        (evc,env,lfun,lmatch,goalopt,debug) rtc)) in
-      VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen
-        evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl)))))
+        ist rtc)) in
+      VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc
+        (interp_constr ist c (Some (pf_concl gl)))))
     | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
       (try
-        let ic =
-	  interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None
-        and ctxt = constr_of_Constr_context (unvarg (List.assoc s lfun)) in
+        let ic = interp_constr ist c None
+        and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in
         begin
           wARNING [<'sTR
             "Cannot pre-constrain the context expression with goal">];
@@ -1009,26 +999,25 @@ and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com =
         errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier";
           print_ast ast>])
     | c ->
-        VArg (Constr (interp_constr_gen evc env (constr_list goalopt lfun)
-          lmatch c (Some (pf_concl gl)))))
+        VArg (Constr (interp_constr ist c (Some (pf_concl gl)))))
   | None ->
     errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
 (* Interprets a CASTEDOPENCOMMAND expression *)
-and cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) com =
-  match goalopt with
+and cast_opencom_interp ist com =
+  match ist.goalopt with
   | Some gl ->
     (match com with
     | Node(_,"EVAL",[c;rtc]) ->
       let redexp = unredexp (unvarg (val_interp
-        (evc,env,lfun,lmatch,goalopt,debug) rtc)) in
-      VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen
-        evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl)))))
+        ist rtc)) in
+      VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc
+        (interp_constr ist c (Some (pf_concl gl)))))
     | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
       (try
-        let ic =
-	  interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None
-        and ctxt = constr_of_Constr_context (unvarg (List.assoc s lfun)) in
+        let ic = interp_constr ist c None
+        and ctxt =
+          constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in
         begin
           wARNING [<'sTR
             "Cannot pre-constrain the context expression with goal">];
@@ -1040,76 +1029,68 @@ and cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) com =
           print_ast ast>])
     | c ->
         VArg
-	  (OpenConstr (interp_openconstr_gen evc env (constr_list goalopt lfun)
-			 lmatch c (Some (pf_concl gl)))))
+	  (OpenConstr (interp_openconstr ist c (Some (pf_concl gl)))))
   | None ->
     errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
 (* Interprets a qualified name. This can be a metavariable to be injected *)
-and qid_interp (evc,env,lfun,lmatch,goalopt,debug) = function
+and qid_interp ist = function
   | Node(loc,"QUALIDARG",p) -> interp_qualid p
   | Node(loc,"QUALIDMETA",[Num(_,n)]) ->
-    Nametab.qualid_of_sp (path_of_const (List.assoc n lmatch))
+    Nametab.qualid_of_sp (path_of_const (List.assoc n ist.lmatch))
   | ast -> 
       anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR
         "Unrecognizable qualid ast: "; print_ast ast>])
 
-and cvt_pattern (evc,env,lfun,lmatch,goalopt,debug) = function
+and cvt_pattern ist = function
   | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) ->
       let occs = List.map num_of_ast nums
       and csr = constr_of_Constr (unvarg (val_interp
-        (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[com])))) in
-      let jdt = Typing.unsafe_machine env evc csr in
+        ist (Node(loc,"COMMAND",[com])))) in
+      let jdt = Typing.unsafe_machine ist.env ist.evc csr in
       (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type)
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
 
-and cvt_unfold (evc,env,lfun,lmatch,goalopt,debug) = function
+and cvt_unfold ist = function
   | Node(_,"UNFOLD", com::nums) ->
-    let qid =
-      qualid_of_Qualid
-        (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) com)) in
-    (List.map num_of_ast nums,glob_const_nvar loc env qid)
+    let qid = qualid_of_Qualid (unvarg (val_interp ist com)) in
+    (List.map num_of_ast nums,glob_const_nvar loc ist.env qid)
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
 
 (* Interprets the arguments of Fold *)
-and cvt_fold (evc,env,lfun,lmatch,goalopt,debug) = function
+and cvt_fold ist = function
   | Node(_,"COMMAND",[c]) as ast ->
-    constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug)
-      ast))
+    constr_of_Constr (unvarg (val_interp ist ast))
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
 
 (* Interprets the reduction flags *)
-and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
+and flag_of_ast ist lf =
   let rec add_flag red = function
     | [] -> red
     | Node(_,"Beta",[])::lf -> add_flag (red_add red fBETA) lf
+    | Node(_,"Delta",[])::Node(loc,"Unf",l)::lf ->
+        let red = red_add_transparent (red_add red fDELTA) all_opaque in
+        let red =
+	  List.fold_right
+	    (fun v red -> 
+	      match glob_const_nvar loc ist.env (qid_interp ist v) with
+		| EvalVarRef id -> red_add red (fVAR id)
+		| EvalConstRef sp -> red_add red (fCONST sp)) l red
+	in add_flag red lf
+    | Node(_,"Delta",[])::Node(loc,"UnfBut",l)::lf ->
+        let red = red_add red fDELTA in
+        let red = red_add_transparent red (Opaque.state()) in
+        let red =
+	  List.fold_right
+	    (fun v red -> 
+	      match glob_const_nvar loc ist.env (qid_interp ist v) with
+		| EvalVarRef id -> red_sub red (fVAR id)
+		| EvalConstRef sp -> red_sub red (fCONST sp)) l red
+	in add_flag red lf
     | Node(_,"Delta",[])::lf ->
-	(match lf with
-	   | Node(loc,"Unf",l)::lf ->
-               let idl=
-		 List.fold_right
-		   (fun v red -> 
-		      match glob_const_nvar loc env
-                        (qid_interp (evc,env,lfun,lmatch,goalopt,debug) v) with
-			| EvalVarRef id -> red_add red (fVAR id)
-			| EvalConstRef sp -> red_add red (fCONST sp)) l red
-	       in add_flag idl lf
-(*
-(id_of_Identifier (unvarg
-		   (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l
-	       in add_flag (red_add red (CONST idl)) lf
-*)
-	   | Node(loc,"UnfBut",l)::lf ->
-               let idl=
-		 List.fold_right
-		   (fun v red -> 
-		      match glob_const_nvar loc env
-                        (qid_interp (evc,env,lfun,lmatch,goalopt,debug)v) with
-			| EvalVarRef id -> red_add red (fVARBUT id)
-			| EvalConstRef sp -> red_add red (fCONSTBUT sp)) l red
-	       in add_flag idl lf
-
-	   | _ -> add_flag (red_add red fDELTA) lf)
+        let red = red_add red fDELTA in
+        let red = red_add_transparent red (Opaque.state()) in
+        add_flag red lf
     | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf
     | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf
     | Node(_,"Evar",[])::lf -> add_flag (red_add red fEVAR) lf
@@ -1122,47 +1103,37 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
   add_flag no_red lf;
 
 (* Interprets a reduction expression *)
-and redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) = function
+and redexp_of_ast ist = function
   | ("Red", []) -> Red false
   | ("Hnf", []) -> Hnf
   | ("Simpl", []) -> Simpl
-  | ("Unfold", ul) ->
-    Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt,debug)) ul)
-  | ("Fold", cl) ->
-    Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt,debug)) cl)
-  | ("Cbv",lf) ->
-    Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf)
-  | ("Lazy",lf) ->
-    Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf)
-  | ("Pattern",lp) ->
-    Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt,debug)) lp)
+  | ("Unfold", ul) -> Unfold (List.map (cvt_unfold ist) ul)
+  | ("Fold", cl) -> Fold (List.map (cvt_fold ist) cl)
+  | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast ist lf)
+  | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast ist lf)
+  | ("Pattern",lp) -> Pattern (List.map (cvt_pattern ist) lp)
   | (s,_) -> invalid_arg ("malformed reduction-expression: "^s)
 
 (* Interprets the patterns of Intro *)
-and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug) = function
+and cvt_intro_pattern ist = function
   | Node(_,"WILDCAR", []) -> WildPat
   | Node(_,"IDENTIFIER", [Nvar(loc,s)]) ->
-    IdPat (id_of_Identifier (unvarg (val_interp
-      (evc,env,lfun,lmatch,goalopt,debug) (Nvar (loc,s)))))
+    IdPat (id_of_Identifier (unvarg (val_interp ist (Nvar (loc,s)))))
   | Node(_,"DISJPATTERN", l) ->
-    DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug))
-      l)
+    DisjPat (List.map (cvt_intro_pattern ist) l)
   | Node(_,"CONJPATTERN", l) ->
-    ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug))
-      l)
+    ConjPat (List.map (cvt_intro_pattern ist) l)
   | Node(_,"LISTPATTERN", l) ->
-    ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug))
-      l)
+    ListPat (List.map (cvt_intro_pattern ist) l)
   | x ->
     errorlabstrm "cvt_intro_pattern"
-      [<'sTR "Not the expected form for an introduction pattern!"; print_ast
-        x>]
+      [<'sTR "Not the expected form for an introduction pattern!";'fNL;
+        print_ast x>]
 
 (* Interprets a pattern of Let *)
-and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function
+and cvt_letpattern ist (o,l) = function
   | Node(_,"HYPPATTERN", Nvar(loc,s)::nums) ->
-    (o,(id_of_Identifier (unvarg (val_interp
-      (evc,env,lfun,lmatch,goalopt,debug)
+    (o,(id_of_Identifier (unvarg (val_interp ist
       (Nvar (loc,s)))),List.map num_of_ast nums)::l)
   | Node(_,"CCLPATTERN", nums) ->
     if o <> None then
@@ -1200,7 +1171,10 @@ let bad_tactic_args s =
 let (inMD,outMD) =
   let add (na,td) = mactab := Gmap.add na td !mactab in
   let cache_md (_,(na,td)) =  
-    let ve=val_interp (Evd.empty,Global.env (),[],[],None,get_debug ()) td 
+    let ve=val_interp
+      {evc=Evd.empty;env=Global.env ();lfun=[];
+       lmatch=[]; goalopt=None; debug=get_debug ()}
+      td 
     in add (na,ve) in 
     declare_object ("TAC-DEFINITION",
        {cache_function  = cache_md;
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index f6be508697..41b105f7bb 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -31,8 +31,12 @@ type value =
 
 (* Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
-  enamed_declarations * Environ.env * (identifier * value) list *
-    (int * constr) list * goal sigma option * debug_info
+  { evc : enamed_declarations;
+    env : Environ.env;
+    lfun : (identifier * value) list;
+    lmatch : (int * constr) list;
+    goalopt : goal sigma option;
+    debug : debug_info }
 
 (* Gives the constr corresponding to a CONSTR [tactic_arg] *)
 val constr_of_Constr : tactic_arg -> constr