path: root/tactics/tacinterp.ml

(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Constrintern
open Closure
open RedFlags
open Declarations
open Entries
open Dyn
open Libobject
open Pattern
open Matching
open Pp
open Rawterm
open Sign
open Tacred
open Util
open Names
open Nameops
open Libnames
open Nametab
open Pfedit
open Proof_type
open Refiner
open Tacmach
open Tactic_debug
open Topconstr
open Ast
open Term
open Termops
open Declare
open Tacexpr
open Safe_typing
open Typing
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 
    (loc,"out_ident",
     str "Syntactic metavariables allowed only in quotations")

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 =
  | VTactic of loc * tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
  | VRTactic of (goal list sigma * validation) (* For Match results *)
                                               (* Not a true value *)
  | VFun of (identifier*value) list * identifier option list * glob_tactic_expr
  | VVoid
  | VInteger of int
  | 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

let locate_tactic_call loc = function
  | VTactic (_,t) -> VTactic (loc,t)
  | v -> v

let catch_error loc tac g =
  try tac g
  with e when loc <> dummy_loc ->
    match e with
      |	Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e))
      |	e -> raise (Stdpp.Exc_located (loc,e))

(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign =
  { lfun : (identifier * value) list;
    lmatch : (int * constr) list;
    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_context tactic_arg *)
let constr_of_VConstr_context = function
  | VConstr_context c -> c
  | _ ->
    anomalylabstrm "constr_of_VConstr_context" (str
      "Not a Constr_context tactic_arg")

(* Displays a value *)
let pr_value env = function
  | VVoid -> str "()"
  | VInteger n -> int n
  | VIdentifier id -> pr_id id
  | VConstr c -> Printer.prterm_env env c
  | VConstr_context c -> Printer.prterm_env env c
  | (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, 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),
     (tactic_out : Dyn.t -> (interp_sign -> raw_tactic_expr))) =
  create "tactic"

let ((value_in : value -> Dyn.t),
     (value_out : Dyn.t -> value)) = create "value"

let tacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
let tacticOut = function
  | TacArg (TacDynamic (_,d)) ->
    if (tag d) = "tactic" then
      tactic_out d
    else
      anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
  | ast ->
    anomalylabstrm "tacticOut"
      (str "Not a Dynamic ast: " (* ++ print_ast ast*) )

let valueIn t = TacDynamic (dummy_loc,value_in t)
let valueOut = function
  | TacDynamic (_,d) ->
    if (tag d) = "value" then
      value_out d
    else
      anomalylabstrm "valueOut" (str "Dynamic tag should be value")
  | ast ->
    anomalylabstrm "valueOut" (str "Not a Dynamic ast: ")

(* To embed constr in Coqast.t *)
let constrIn t = CDynamic (dummy_loc,Pretyping.constr_in t)
let constrOut = function
  | CDynamic (_,d) ->
    if (Dyn.tag d) = "constr" then
      Pretyping.constr_out d
    else
      anomalylabstrm "constrOut" (str "Dynamic tag should be constr")
  | ast ->
    anomalylabstrm "constrOut" (str "Not a Dynamic ast")
let loc = dummy_loc

(* Table of interpretation functions *)
let interp_tab =
  (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t)

(* Adds an interpretation function *)
let interp_add (ast_typ,interp_fun) =
  try
    Hashtbl.add interp_tab ast_typ interp_fun
  with
      Failure _ ->
        errorlabstrm "interp_add"
          (str "Cannot add the interpretation function for " ++ str ast_typ ++            str " twice")

(* Adds a possible existing interpretation function *)
let overwriting_interp_add (ast_typ,interp_fun) =
  if Hashtbl.mem interp_tab ast_typ then
  begin
    Hashtbl.remove interp_tab ast_typ;
    warning ("Overwriting definition of tactic interpreter command " ^ ast_typ)
  end;
  Hashtbl.add interp_tab ast_typ interp_fun

(* Finds the interpretation function corresponding to a given ast type *)
let look_for_interp = Hashtbl.find interp_tab

(* Globalizes the identifier *)

let find_reference env qid =
  (* We first look for a variable of the current proof *)
  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 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 env v ++ 
       str "cannot be coerced to a reference")

(* turns a value into an evaluable reference *)
let error_not_evaluable s =
  errorlabstrm "evalref_of_ref" 
    (str "Cannot coerce" ++ spc ()  ++ s ++ spc () ++
     str "to an evaluable reference")

let coerce_to_evaluable_ref env c =
  let ev = match c with
    | VConstr c when isConst c -> EvalConstRef (destConst c)
    | VConstr c when isVar c -> EvalVarRef (destVar c)
(*    | VIdentifier id -> EvalVarRef id*)
    | _ -> error_not_evaluable (pr_value env c)
  in
  if not (Tacred.is_evaluable env ev) then
    error_not_evaluable (pr_value env c);
  ev

let coerce_to_inductive = function
  | VConstr c when isInd c -> destInd c
  | x ->
      try
	let r = match x with
	  | VConstr c -> reference_of_constr c
	  | _ -> failwith "" in
	errorlabstrm "coerce_to_inductive"
          (Printer.pr_global r ++ str " is not an inductive type")
      with _ ->
	errorlabstrm "coerce_to_inductive"
          (str "Found an argument which should be an inductive type")

(* Summary and Object declaration *)
let mactab = ref Gmap.empty

let lookup r = Gmap.find r !mactab

let _ =
  let init () = mactab := Gmap.empty in
  let freeze () = !mactab in
  let unfreeze fs = mactab := fs in
  Summary.declare_summary "tactic-definition"
    { Summary.freeze_function   = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function     = init;
      Summary.survive_section   = false }

(* Interpretation of extra generic arguments *)
type glob_sign = {
  ltacvars : identifier list * identifier list;
     (* ltac variables and the subset of vars introduced by Intro/Let/... *)
  ltacrecvars : (identifier * ltac_constant) list;
     (* ltac recursive names *)
  metavars : int list;
     (* metavariables introduced by patterns *)
  gsigma : Evd.evar_map;
  genv : Environ.env }

type interp_genarg_type =
  (glob_sign -> raw_generic_argument -> glob_generic_argument) *
  (interp_sign -> goal sigma -> glob_generic_argument -> 
    closed_generic_argument) *
  (Names.substitution -> glob_generic_argument -> glob_generic_argument)

let extragenargtab =
  ref (Gmap.empty : (string,interp_genarg_type) Gmap.t)
let add_interp_genarg id f =
  extragenargtab := Gmap.add id f !extragenargtab
let lookup_genarg id = 
  try Gmap.find id !extragenargtab
  with Not_found -> failwith ("No interpretation function found for entry "^id)

let lookup_genarg_glob   id = let (f,_,_) = lookup_genarg id in f
let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f
let lookup_genarg_subst  id = let (_,_,f) = lookup_genarg id in f

(* Unboxes VRec *)
let unrec = function
  | VRec v -> !v
  | a -> a

(*****************)
(* Globalization *)
(*****************)

(* We have identifier <| global_reference <| constr *)

let find_ident id sign = 
  List.mem id (fst sign.ltacvars) or 
  List.mem id (ids_of_named_context (Environ.named_context sign.genv))

let find_recvar qid sign = List.assoc qid sign.ltacrecvars

(* a "var" is a ltac var or a var introduced by an intro tactic *)
let find_var id sign = List.mem id (fst sign.ltacvars)

(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
let find_ctxvar id sign = List.mem id (snd sign.ltacvars)

(* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign)

let find_hyp id sign =
  List.mem id (ids_of_named_context (Environ.named_context sign.genv))

(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
(* be fresh in which case it is binding later on *)
let intern_ident l ist id =
  (* We use identifier both for variables and new names; thus nothing to do *)
  if find_ident id ist then () else l:=(id::fst !l,id::snd !l);
  id

let intern_name l ist = function
  | Anonymous -> Anonymous
  | Name id -> Name (intern_ident l ist id)

let vars_of_ist (lfun,_,_,env) =
  List.fold_left (fun s id -> Idset.add id s)
    (vars_of_env env) lfun

let get_current_context () =
    try Pfedit.get_current_goal_context ()
    with e when Logic.catchable_exception e -> 
      (Evd.empty, Global.env())

let strict_check = ref false

(* Globalize a name which must be bound -- actually just check it is bound *)
let intern_hyp ist (loc,id) =
  let (_,env) = get_current_context () in
  if (not !strict_check) or find_ident id ist then id
  else
    Pretype_errors.error_var_not_found_loc loc id

let intern_lochyp ist (_loc,_ as locid) = (loc,intern_hyp ist locid)

let error_unbound_metanum loc n =
  user_err_loc
    (loc,"intern_qualid_or_metanum", str "?" ++ int n ++ str " is unbound")

let intern_metanum sign loc n =
  if List.mem n sign.metavars then n else error_unbound_metanum loc n

let intern_hyp_or_metanum ist = function
  | AN id -> AN (intern_hyp ist (loc,id))
  | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)

let intern_inductive ist = function
  | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
  | r -> ArgArg (Nametab.global_inductive r)

let intern_or_metanum f ist = function
  | AN x -> AN (f ist x)
  | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)

let intern_global_reference ist = function
  | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id)
  | r -> ArgArg (loc,Nametab.global r)

let intern_tac_ref ist = function
  | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
  | Ident (loc,id) ->
      ArgArg
        (try find_recvar id ist 
         with Not_found -> locate_tactic (make_short_qualid id))
  | r -> 
      let (loc,qid) = qualid_of_reference r in
      ArgArg (locate_tactic qid)

let intern_tactic_reference ist r =
  try intern_tac_ref ist r
  with Not_found -> 
    let (loc,qid) = qualid_of_reference r in
    error_global_not_found_loc loc qid

let intern_constr_reference strict ist = function
  | Ident (loc,id) as x when find_hyp id ist ->
      RVar (loc,id), if strict then None else Some (CRef x)
  | r ->
      let loc,qid = qualid_of_reference r in
      RRef (loc,Nametab.locate qid), (*Long names can't be Intro's names*) None

let intern_reference strict ist r =
  try Reference (intern_tac_ref ist r)
  with Not_found -> 
  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
  with Not_found ->
  match r with
    | Ident (loc,id) when not strict -> Identifier id
    | _ -> 
        let (loc,qid) = qualid_of_reference r in
        error_global_not_found_loc loc qid

let rec intern_intro_pattern lf ist = function
  | IntroOrAndPattern l ->
      IntroOrAndPattern (List.map (List.map (intern_intro_pattern lf ist)) l)
  | IntroWildcard ->
      IntroWildcard
  | IntroIdentifier id ->
      IntroIdentifier (intern_ident lf ist id)

let intern_quantified_hypothesis ist x =
  (* We use identifier both for variables and quantified hyps (no way to
     statically check the existence of a quantified hyp); thus nothing to do *)
  x

let intern_constr {ltacvars=lfun; metavars=lmatch; gsigma=sigma; genv=env} c =
  let c' =
    Constrintern.for_grammar (Constrintern.interp_rawconstr_gen false
      sigma env [] (Some lmatch) (fst lfun,[])) c
  in (c',if !strict_check then None else Some c)

(* Globalize bindings *)
let intern_binding ist (loc,b,c) =
  (loc,intern_quantified_hypothesis ist b,intern_constr ist c)

let intern_bindings ist = function
  | NoBindings -> NoBindings
  | ImplicitBindings l -> ImplicitBindings (List.map (intern_constr ist) l)
  | ExplicitBindings l -> ExplicitBindings (List.map (intern_binding ist) l)

let intern_constr_with_bindings ist (c,bl) =
  (intern_constr ist c, intern_bindings ist bl)

let intern_clause_pattern ist (l,occl) =
  let rec check = function
    | (hyp,l) :: rest -> 
	let (_loc,_ as id) = skip_metaid hyp in
	((loc,intern_hyp ist id),l)::(check rest)
    | [] -> []
  in (l,check occl)

let intern_induction_arg ist = function
  | ElimOnConstr c -> ElimOnConstr (intern_constr ist c)
  | ElimOnAnonHyp n as x -> x
  | ElimOnIdent (_loc,id) as x -> ElimOnIdent (loc,id)

(* Globalizes a reduction expression *)
let intern_evaluable_or_metanum ist = function
  | AN qid ->
      let e = match qid with
        | Ident (loc,id) when find_ctxvar id ist ->
            ArgArg (EvalVarRef id, Some id)
        | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id)
        | r -> 
            let e = match fst (intern_constr_reference true ist r) with
            | RRef (_,ConstRef c) -> EvalConstRef c
            | RRef (_,VarRef c) | RVar (_,c) -> EvalVarRef c
            | _ -> error_not_evaluable (pr_reference r) in
            let short_name = match r with
              | Ident (_,id) when not !strict_check -> Some id
              | _ -> None in
            ArgArg (e,short_name) 
      in AN e
  | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)

let intern_unfold ist (l,qid) = (l,intern_evaluable_or_metanum ist qid)

let intern_flag ist red =
  { red with rConst = List.map (intern_evaluable_or_metanum ist) red.rConst }

let intern_constr_occurrence ist (l,c) = (l,intern_constr ist c)

let intern_redexp ist = function
  | Unfold l -> Unfold (List.map (intern_unfold ist) l)
  | Fold l -> Fold (List.map (intern_constr ist) l)
  | Cbv f -> Cbv (intern_flag ist f)
  | Lazy f -> Lazy (intern_flag ist f)
  | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
  | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
  | (Red _ | Hnf as r) -> r
  | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c)

(* Interprets an hypothesis name *)
let intern_hyp_location ist = function
  | InHyp id ->
      let (_loc,_ as id) = skip_metaid id in
      InHyp (loc,intern_hyp ist id)
  | InHypType id -> 
      let (_loc,_ as id) = skip_metaid id in
      InHypType (loc,intern_hyp ist id)

(* Reads a pattern *)
let intern_pattern evc env lfun = function
  | Subterm (ido,pc) ->
      let lfun = List.map (fun id -> (id, mkVar id)) lfun in
      let (metas,pat) = interp_constrpattern_gen evc env (lfun,[]) pc  in
      metas, Subterm (ido,pat)
  | Term pc ->
      let lfun = List.map (fun id -> (id, mkVar id)) lfun in
      let (metas,pat) = interp_constrpattern_gen evc env (lfun,[]) pc  in
      metas, Term pat

let intern_constr_may_eval ist = function
  | ConstrEval (r,c) -> ConstrEval (intern_redexp ist r,intern_constr ist c)
  | ConstrContext (locid,c) ->
      ConstrContext ((loc,intern_hyp ist locid),intern_constr ist c)
  | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
  | ConstrTerm c -> ConstrTerm (intern_constr ist c)

(* Reads the hypotheses of a Match Context rule *)
let rec intern_match_context_hyps evc env lfun = function
  | (NoHypId mp)::tl ->
      let metas1, pat = intern_pattern evc env lfun mp in
      let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in
      lfun, metas1@metas2, (NoHypId pat)::hyps
  | (Hyp ((_,s) as locs,mp))::tl ->
      let metas1, pat = intern_pattern evc env lfun mp in
      let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in
      s::lfun, metas1@metas2, Hyp (locs,pat)::hyps
  | [] -> lfun, [], []

(* Utilities *)
let rec filter_some = function
  | None :: l -> filter_some l
  | Some a :: l -> a :: filter_some l
  | [] -> []

let extract_names lrc =
  List.fold_right 
    (fun ((loc,name),_) l ->
      if List.mem name l then
	user_err_loc
	  (loc, "intern_tactic", str "This variable is bound several times");
      name::l)
    lrc []

let extract_let_names lrc =
  List.fold_right 
    (fun ((loc,name),_,_) l ->
      if List.mem name l then
	user_err_loc
	  (loc, "glob_tactic", str "This variable is bound several times");
      name::l)
    lrc []

(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
let rec intern_atomic lf ist x =
  match (x:raw_atomic_tactic_expr) with 
  (* Basic tactics *)
  | TacIntroPattern l ->
      TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
  | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
  | TacIntroMove (ido,ido') ->
      TacIntroMove (option_app (intern_ident lf ist) ido,
          option_app (fun (_loc,_ as x) -> (loc,intern_hyp ist x)) ido')
  | TacAssumption -> TacAssumption
  | TacExact c -> TacExact (intern_constr ist c)
  | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
  | TacElim (cb,cbo) ->
      TacElim (intern_constr_with_bindings ist cb,
               option_app (intern_constr_with_bindings ist) cbo)
  | TacElimType c -> TacElimType (intern_constr ist c)
  | TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
  | TacCaseType c -> TacCaseType (intern_constr ist c)
  | TacFix (idopt,n) -> TacFix (option_app (intern_ident lf ist) idopt,n)
  | TacMutualFix (id,n,l) ->
      let f (id,n,c) = (intern_ident lf ist id,n,intern_constr ist c) in
      TacMutualFix (intern_ident lf ist id, n, List.map f l)
  | TacCofix idopt -> TacCofix (option_app (intern_ident lf ist) idopt)
  | TacMutualCofix (id,l) ->
      let f (id,c) = (intern_ident lf ist id,intern_constr ist c) in
      TacMutualCofix (intern_ident lf ist id, List.map f l)
  | TacCut c -> TacCut (intern_constr ist c)
  | TacTrueCut (ido,c) ->
      TacTrueCut (option_app (intern_ident lf ist) ido, intern_constr ist c)
  | TacForward (b,na,c) -> TacForward (b,intern_name lf ist na,intern_constr ist c)
  | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
  | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
  | TacLetTac (id,c,clp) ->
      let id = intern_ident lf ist id in
      TacLetTac (id,intern_constr ist c,intern_clause_pattern ist clp)
  | TacInstantiate (n,c) -> TacInstantiate (n,intern_constr ist c)

  (* Automation tactics *)
  | TacTrivial l -> TacTrivial l
  | TacAuto (n,l) -> TacAuto (n,l)
  | TacAutoTDB n -> TacAutoTDB n
  | TacDestructHyp (b,(_loc,_ as id)) ->
      TacDestructHyp(b,(loc,intern_hyp ist id))
  | TacDestructConcl -> TacDestructConcl
  | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
  | TacDAuto (n,p) -> TacDAuto (n,p)

  (* Derived basic tactics *)
  | TacOldInduction h -> TacOldInduction (intern_quantified_hypothesis ist h)
  | TacNewInduction (c,cbo,ids) ->
      TacNewInduction (intern_induction_arg ist c,
               option_app (intern_constr_with_bindings ist) cbo,
               List.map (List.map (intern_ident lf ist)) ids)
  | TacOldDestruct h -> TacOldDestruct (intern_quantified_hypothesis ist h)
  | TacNewDestruct (c,cbo,ids) ->
      TacNewDestruct (intern_induction_arg ist c,
               option_app (intern_constr_with_bindings ist) cbo,
               List.map (List.map (intern_ident lf ist)) ids)
  | TacDoubleInduction (h1,h2) ->
      let h1 = intern_quantified_hypothesis ist h1 in
      let h2 = intern_quantified_hypothesis ist h2 in
      TacDoubleInduction (h1,h2)
  | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c)
  | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c)
  | TacDecompose (l,c) ->
      let l = List.map (intern_or_metanum intern_inductive ist) l in
      TacDecompose (l,intern_constr ist c)
  | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
  | TacLApply c -> TacLApply (intern_constr ist c)

  (* Context management *)
  | TacClear l -> TacClear (List.map (intern_hyp_or_metanum ist) l)
  | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metanum ist) l)
  | TacMove (dep,id1,id2) ->
    TacMove (dep,intern_lochyp ist id1,intern_lochyp ist id2)
  | TacRename (id1,id2) -> TacRename (intern_lochyp ist id1, intern_lochyp ist id2)

  (* Constructors *)
  | TacLeft bl -> TacLeft (intern_bindings ist bl)
  | TacRight bl -> TacRight (intern_bindings ist bl)
  | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
  | TacAnyConstructor t -> TacAnyConstructor (option_app (intern_tactic ist) t)
  | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)

  (* Conversion *)
  | TacReduce (r,cl) ->
      TacReduce (intern_redexp ist r, List.map (intern_hyp_location ist) cl)
  | TacChange (occl,c,cl) ->
      TacChange (option_app (intern_constr_occurrence ist) occl,
        intern_constr ist c, List.map (intern_hyp_location ist) cl)

  (* Equivalence relations *)
  | TacReflexivity -> TacReflexivity
  | TacSymmetry -> TacSymmetry
  | TacTransitivity c -> TacTransitivity (intern_constr ist c)

  (* For extensions *)
  | TacExtend (_loc,opn,l) ->
      let _ = lookup_tactic opn in
      TacExtend (loc,opn,List.map (intern_genarg ist) l)
  | TacAlias (s,l,body) ->
      TacAlias (s,List.map (fun (id,a) -> (id,intern_genarg ist a)) l,intern_tactic ist body)

and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr)

and intern_tactic_seq ist = function
  | TacAtom (_loc,t) ->
      let lf = ref ist.ltacvars in
      let t = intern_atomic lf ist t in
      !lf, TacAtom (loc, t)
  | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
  | TacLetRecIn (lrc,u) ->
      let names = extract_names lrc in
      let (l1,l2) = ist.ltacvars in
      let ist = { ist with ltacvars = (names@l1,l2) } in
      let lrc = List.map (fun (n,b) -> (n,intern_tactic_fun ist b)) lrc in
      ist.ltacvars, TacLetRecIn (lrc,intern_tactic ist u)
  | TacLetIn (l,u) ->
      let l = List.map
        (fun (n,c,b) ->
          (n,option_app (intern_constr_may_eval ist) c, intern_tacarg !strict_check ist b)) l in
      let (l1,l2) = ist.ltacvars in
      let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
      ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
  | TacLetCut l ->
      let f (n,c,t) = (n,intern_constr_may_eval ist c,intern_tacarg !strict_check ist t) in
      ist.ltacvars, TacLetCut (List.map f l)
  | TacMatchContext (lr,lmr) ->
      ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
  | TacMatch (c,lmr) ->
      ist.ltacvars, TacMatch (intern_constr_may_eval ist c,intern_match_rule ist lmr)
  | TacId -> ist.ltacvars, TacId
  | TacFail _ as x -> ist.ltacvars, x
  | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
  | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
  | TacThen (t1,t2) ->
      let lfun', t1 = intern_tactic_seq ist t1 in
      let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
      lfun'', TacThen (t1,t2)
  | TacThens (t,tl) ->
      let lfun', t = intern_tactic_seq ist t in
      (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
      lfun',
      TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
  | TacDo (n,tac) -> ist.ltacvars, TacDo (n,intern_tactic ist tac)
  | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
  | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
  | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
  | TacOrelse (tac1,tac2) ->
      ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2)
  | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l)
  | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l)
  | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a)

and intern_tactic_fun ist (var,body) = 
  let (l1,l2) = ist.ltacvars in
  let lfun' = List.rev_append (filter_some var) l1 in
  (var,intern_tactic { ist with ltacvars = (lfun',l2) } body)

and intern_tacarg strict ist = function
  | TacVoid -> TacVoid
  | Reference r -> intern_reference strict ist r
  | Identifier id -> anomaly "Not used only in raw_tactic_expr"
  | Integer n -> Integer n
  | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
  | MetaIdArg (_loc,_) -> error_syntactic_metavariables_not_allowed loc
  | TacCall (_loc,f,l) ->
      TacCall (_loc,
        intern_tactic_reference ist f,
        List.map (intern_tacarg !strict_check ist) l)
  | Tacexp t -> Tacexp (intern_tactic ist t)
  | TacDynamic(_,t) as x ->
      (match tag t with
	| "tactic" | "value" | "constr" -> x
	| s -> anomaly_loc (loc, "",
                 str "Unknown dynamic: <" ++ str s ++ str ">"))

(* Reads the rules of a Match Context or a Match *)
and intern_match_rule ist = function
  | (All tc)::tl ->
      All (intern_tactic ist tc) :: (intern_match_rule ist tl)
  | (Pat (rl,mp,tc))::tl ->
      let {ltacvars=(lfun,l2); metavars=lmeta; gsigma=sigma; genv=env} = ist in
      let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
      let metas2,pat = intern_pattern sigma env lfun mp in
      let metas = list_uniquize (metas1@metas2@lmeta) in
      let ist' = { ist with ltacvars = (lfun',l2); metavars = metas } in
      Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
  | [] -> []

and intern_genarg ist x =
  match genarg_tag x with
  | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x)
  | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
  | IntOrVarArgType ->
      let f = function
	| ArgVar (_loc,id) -> ArgVar (loc,intern_hyp ist (loc,id))
	| ArgArg n as x -> x in
      in_gen globwit_int_or_var (f (out_gen rawwit_int_or_var x))
  | StringArgType ->
      in_gen globwit_string (out_gen rawwit_string x)
  | PreIdentArgType ->
      in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
  | IdentArgType ->
      in_gen globwit_ident (intern_hyp ist (dummy_loc,out_gen rawwit_ident x))
  | RefArgType ->
      in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
  | SortArgType ->
      in_gen globwit_sort (out_gen rawwit_sort x)
  | ConstrArgType ->
      in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x))
  | ConstrMayEvalArgType ->
      in_gen globwit_constr_may_eval 
        (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
  | QuantHypArgType ->
      in_gen globwit_quant_hyp
        (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
  | RedExprArgType ->
      in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
  | TacticArgType ->
      in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x))
  | CastedOpenConstrArgType ->
      in_gen globwit_casted_open_constr 
        (intern_constr ist (out_gen rawwit_casted_open_constr x))
  | ConstrWithBindingsArgType ->
      in_gen globwit_constr_with_bindings
        (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
  | List0ArgType _ -> app_list0 (intern_genarg ist) x
  | List1ArgType _ -> app_list1 (intern_genarg ist) x
  | OptArgType _ -> app_opt (intern_genarg ist) x
  | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
  | ExtraArgType s -> lookup_genarg_glob s ist x

(************* End globalization ************)

(***************************************************************************)
(* Evaluation/interpretation *)

(* Associates variables with values and gives the remaining variables and
   values *)
let head_with_value (lvar,lval) =
  let rec head_with_value_rec lacc = function
    | ([],[]) -> (lacc,[],[])
    | (vr::tvr,ve::tve) ->
      (match vr with
      |	None -> head_with_value_rec lacc (tvr,tve)
      | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
    | (vr,[]) -> (lacc,vr,[])
    | ([],ve) -> (lacc,[],ve)
  in
    head_with_value_rec [] (lvar,lval)

(* Gives a context couple if there is a context identifier *)
let give_context ctxt = function
  | None -> []
  | Some id -> [id,VConstr_context ctxt]

(* Reads a pattern by substituing vars of lfun *)
let eval_pattern lfun c = 
  let lvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lfun in
  instantiate_pattern lvar c

let read_pattern evc env lfun = function
  | Subterm (ido,pc) -> Subterm (ido,eval_pattern lfun pc)
  | Term pc -> Term (eval_pattern lfun pc)

(* Reads the hypotheses of a Match Context rule *)
let rec read_match_context_hyps evc env lfun lidh = function
  | (NoHypId mp)::tl ->
    (NoHypId (read_pattern evc env lfun mp))::
      (read_match_context_hyps evc env lfun lidh tl)
  | (Hyp ((loc,id) as locid,mp))::tl ->
    if List.mem id lidh then
      user_err_loc (loc,"Tacinterp.read_match_context_hyps",
      str ("Hypothesis pattern-matching variable "^(string_of_id id)^
           " used twice in the same pattern"))
    else
    (Hyp (locid,read_pattern evc env lfun mp))::
      (read_match_context_hyps evc env lfun (id::lidh) tl)
  | [] -> []

(* Reads the rules of a Match Context or a Match *)
let rec read_match_rule evc env lfun = function
  | (All tc)::tl -> (All tc)::(read_match_rule evc env lfun tl)
  | (Pat (rl,mp,tc))::tl ->
      Pat (read_match_context_hyps evc env lfun [] rl,
      read_pattern evc env lfun mp,tc)
       ::(read_match_rule evc env lfun tl)
  | [] -> []

(* For Match Context and Match *)
exception No_match
exception Not_coherent_metas
exception Eval_fail of string

let is_failure = function
  | FailError _ | Stdpp.Exc_located (_,FailError _) -> true
  | _ -> false

let is_match_catchable = function
  | No_match | Eval_fail _ -> true
  | e -> is_failure e or Logic.catchable_exception e

(* Verifies if the matched list is coherent with respect to lcm *)
let rec verify_metas_coherence gl lcm = function
  | (num,csr)::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
  | [] -> []

(* Tries to match a pattern and a constr *)
let apply_matching pat csr =
  try
    (matches pat csr)
  with
     PatternMatchingFailure -> raise No_match

(* Tries to match one hypothesis pattern with a list of hypotheses *)
let apply_one_mhyp_context ist env 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]
    | NoHypId _ -> [] 
  and get_info_pattern = function
    | Hyp((_,idpat),pat) -> (Some idpat,pat)
    | NoHypId pat -> (None,pat) in
  let rec apply_one_mhyp_context_rec ist env mhyp lhyps_acc nocc = function
    | (id,hyp)::tl ->
      (match (get_pattern mhyp) with
      | Term t ->
        (try
          let lmeta = 
            verify_metas_coherence gl lmatch (matches t hyp) in
          (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None)
         with | PatternMatchingFailure | Not_coherent_metas ->
          apply_one_mhyp_context_rec ist env 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 gl lmatch lm in
          (get_id_couple id mhyp,give_context ctxt
            ic,lmeta,tl,(id,hyp),Some nocc)
         with
        | NextOccurrence _ ->
          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl
        | Not_coherent_metas ->
          apply_one_mhyp_context_rec ist env mhyp lhyps_acc (nocc + 1)
                                     ((id,hyp)::tl)))
    | [] ->
      begin
        db_hyp_pattern_failure ist.debug env (get_info_pattern mhyp);
        raise No_match
      end in
  let nocc =
    match noccopt with
    | None -> 0
    | Some n -> n in
  apply_one_mhyp_context_rec ist env mhyp [] nocc lhyps

(* Gets the identifier of the pattern if it exists *)
let get_id_pattern = function
  | [] -> None
  | [(id,_)] -> Some id
  | _ -> assert false

(*
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")

let constr_to_qid loc c =
  try shortest_qualid_of_global Idset.empty (reference_of_constr c)
  with _ -> invalid_arg_loc (loc, "Not a global reference")

(* Check for LetTac *)
let check_clause_pattern ist gl (l,occl) =
  let sign = pf_hyps gl in
  let rec check acc = function
    | ((_,hyp),l) :: rest ->
	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

(* Sets the debugger mode *)
let set_debug pos = debug := pos

(* Gives the state of debug *)
let get_debug () = !debug

(* Interprets an identifier which must be fresh *)
let eval_ident ist id =
  try match List.assoc id ist.lfun with
  | VIdentifier id -> id
  | VConstr c as v when isVar c ->
      (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *)
      (* c is then expected not to belong to the proof context *)
      (* would be checkable if env were known from eval_ident *)
      destVar c
  | _ -> user_err_loc(loc,"eval_ident",str "should be bound to an identifier")
  with Not_found -> id

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 is_variable env id =
  List.mem id (ids_of_named_context (Environ.named_context env))

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

(* 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
    user_err_loc (loc,"eval_variable",pr_id id ++ str " not found")

let interp_hyp = eval_variable

let eval_name ist = function
  | Anonymous -> Anonymous
  | Name id -> Name (eval_ident ist id)

let interp_hyp_or_metanum 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 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")

(* Interprets a qualified name *)
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 env (loc,make_short_qualid id)

let interp_reference ist env = function
  | ArgArg (_,r) -> r
  | ArgVar (loc,id) -> coerce_to_reference env (unrec (List.assoc id ist.lfun))

let pf_interp_reference ist gl = interp_reference ist (pf_env gl)

let interp_inductive_or_metanum ist = function
  | MetaNum (loc,n) ->
      coerce_to_inductive (VConstr (List.assoc n ist.lmatch))
  | AN r -> match r with
      | ArgArg r -> r
      | ArgVar (_,id) -> 
          coerce_to_inductive (unrec (List.assoc id ist.lfun))

let interp_evaluable_or_metanum ist env = function
  | MetaNum (loc,n) ->
      coerce_to_evaluable_ref env (VConstr (List.assoc n ist.lmatch))
  | AN r -> match r with
      | ArgArg (r,Some id) ->
          (* Maybe [id] has been introduced by Intro-like tactics *)
          (try match Environ.lookup_named id env with
            | (_,Some _,_) -> EvalVarRef id
            | _ -> error_not_evaluable (pr_id id)
          with Not_found -> r)
      | ArgArg (r,None) -> r
      | ArgVar (_,id) -> 
          coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))

(* Interprets an hypothesis name *)
let interp_hyp_location ist gl = function
  | InHyp id -> InHyp (interp_hyp ist gl id)
  | InHypType id -> InHypType (interp_hyp ist gl id)

let eval_opt_ident ist = option_app (eval_ident ist)

(* Interpretation of constructions *)

(* 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 retype_list sigma env lst =
  List.fold_right (fun (x,csr) a ->
    try (x,Retyping.get_judgment_of env sigma csr)::a with
    | Anomaly _ -> a) lst []

let interp_casted_constr ocl ist sigma env (c,ce) =
  let (l1,l2) = constr_list ist env in
  let rtype lst = retype_list sigma env lst in
  let csr = 
    match ce with
    | None ->
	Pretyping.understand_gen sigma env (rtype l1) (rtype ist.lmatch) ocl c
      (* If at toplevel (ce<>None), the error can be due to an incorrect
         context at globalization time: we retype with the now known
         intros/lettac/inversion hypothesis names *)
    | Some c -> interp_constr_gen sigma env (l1,l2) ist.lmatch c ocl
  in
  db_constr ist.debug env csr;
  csr

let interp_constr ist sigma env c =
  interp_casted_constr None ist sigma env c

(* Interprets an open constr expression casted by the current goal *)
let pf_interp_casted_openconstr ist gl (c,ce) =
  let sigma = project gl in
  let env = pf_env gl in
  let (ltacvar,l) = constr_list ist env in
  let rtype lst = retype_list sigma env lst in
  let ocl = Some (pf_concl gl) in
  match ce with
  | None ->
      Pretyping.understand_gen_tcc sigma env (rtype ltacvar) (rtype ist.lmatch)
      ocl c
    (* If at toplevel (ce<>None), the error can be due to an incorrect
       context at globalization time: we retype with the now known
       intros/lettac/inversion hypothesis names *)
  | Some c -> interp_openconstr_gen sigma env (ltacvar,l) ist.lmatch c ocl

(* Interprets a constr expression *)
let pf_interp_constr ist gl =
  interp_constr ist (project gl) (pf_env gl)

(* Interprets a constr expression casted by the current goal *)
let pf_interp_casted_constr ist gl c =
  interp_casted_constr (Some(pf_concl gl)) ist (project gl) (pf_env gl) c

(* Interprets a reduction expression *)
let interp_unfold ist env (l,qid) =
  (l,interp_evaluable_or_metanum ist env qid)

let interp_flag ist env red =
  { red
    with rConst = List.map (interp_evaluable_or_metanum ist env) red.rConst }

let interp_pattern ist sigma env (l,c) = (l,interp_constr ist sigma env c)

let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl)

let redexp_interp ist sigma env = function
  | Unfold l -> Unfold (List.map (interp_unfold ist env) l)
  | Fold l -> Fold (List.map (interp_constr ist sigma env) l)
  | Cbv f -> Cbv (interp_flag ist env f)
  | Lazy f -> Lazy (interp_flag ist env f)
  | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
  | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
  | (Red _ |  Hnf as r) -> r
  | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c)

let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)

let interp_may_eval f ist gl = function
  | ConstrEval (r,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 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, "interp_may_eval",
	    str "Unbound context identifier" ++ pr_id s))
  | 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 interp_constr_may_eval ist gl c =
  let csr = interp_may_eval pf_interp_constr ist gl c in
  begin
    db_constr ist.debug (pf_env gl) csr;
    csr
  end

let rec interp_intro_pattern ist = function
  | IntroOrAndPattern l ->
      IntroOrAndPattern (List.map (List.map (interp_intro_pattern ist)) l)
  | IntroWildcard ->
      IntroWildcard
  | IntroIdentifier id ->
      IntroIdentifier (eval_ident ist id)

(* 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 ->
      try match List.assoc id ist.lfun with
	| VInteger n -> AnonHyp n
	| VIdentifier id -> NamedHyp id
	| v -> NamedHyp (variable_of_value (pf_env gl) v)
      with Not_found -> NamedHyp id

let interp_induction_arg ist gl = function
  | ElimOnConstr c -> ElimOnConstr (pf_interp_constr ist gl c)
  | ElimOnAnonHyp n as x -> x
  | ElimOnIdent (loc,id) ->
      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
      else ElimOnConstr	(pf_interp_constr ist gl (RVar (loc,id),None))

let interp_binding ist gl (loc,b,c) =
  (loc,interp_quantified_hypothesis ist gl b,pf_interp_constr ist gl c)

let interp_bindings ist gl = function
| NoBindings -> NoBindings
| ImplicitBindings l -> ImplicitBindings (List.map (pf_interp_constr ist gl) l)
| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l)

let interp_constr_with_bindings ist gl (c,bl) =
  (pf_interp_constr ist gl c, interp_bindings ist gl bl)

(* Interprets an l-tac expression into a value *)
let rec val_interp ist gl (tac:glob_tactic_expr) =

  let ist = match ist.debug with
  | DebugOn | Run _ -> {ist with debug = debug_prompt gl ist.debug tac }
  | _ -> ist in

  match tac with
  (* Immediate evaluation *)
  | TacFun (it,body) -> VFun (ist.lfun,it,body)
  | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u
  | TacLetIn (l,u) ->
      let addlfun = interp_letin 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 -> interp_tacarg ist gl a
  (* Delayed evaluation *)
  | t -> VTactic (dummy_loc,eval_tactic ist t)

and eval_tactic ist = function
  | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
  | TacFun (it,body) -> assert false
  | TacLetRecIn (lrc,u) -> assert false
  | TacLetIn (l,u) -> assert false
  | TacLetCut l -> letcut_interp ist l
  | TacMatchContext _ -> assert false
  | TacMatch (c,lmr) -> assert false
  | TacId -> tclIDTAC
  | TacFail (n,s) -> tclFAIL n s
  | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
  | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
  | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
  | TacThens (t,tl) ->
      tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl)
  | TacDo (n,tac) -> tclDO n (interp_tactic ist tac)
  | TacTry tac -> tclTRY (interp_tactic ist tac)
  | TacInfo tac -> tclINFO (interp_tactic ist tac)
  | TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
  | TacOrelse (tac1,tac2) ->
        tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
  | TacFirst l -> tclFIRST (List.map (interp_tactic ist) l)
  | TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l)
  | TacArg a -> assert false

and interp_ltac_reference isapplied ist gl = function
  | ArgVar (loc,id) -> unrec (List.assoc id ist.lfun)
  | ArgArg qid ->
      let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid) in
      if isapplied then v else locate_tactic_call loc v

and interp_tacarg ist gl = function
  | TacVoid -> VVoid
  | Reference r -> interp_ltac_reference false ist gl r
  | Integer n -> VInteger n
  | Identifier id -> VIdentifier id
  | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
  | MetaIdArg (loc,id) ->
      (try (* $id can occur in Grammar tactic... *)
        (unrec (List.assoc (id_of_string id) ist.lfun))
      with
        | Not_found -> error_syntactic_metavariables_not_allowed loc)
  | TacCall (loc,f,l) ->
      let fv = interp_ltac_reference true ist gl f
      and largs = List.map (interp_tacarg ist gl) l in
      List.iter check_is_value largs;
      interp_app 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 gl
          (intern_tactic {
            ltacvars = (List.map fst ist.lfun,[]); ltacrecvars = [];
            metavars = List.map fst ist.lmatch;
            gsigma = project gl; genv = pf_env gl }
            (f ist))
      else if tg = "value" then
        value_out t
      else if tg = "constr" then
        VConstr (Pretyping.constr_out t)
      else
        anomaly_loc (loc, "Tacinterp.val_interp",
          (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))

(* Interprets an application node *)
and interp_app ist gl fv largs loc =
  match fv with
    | VFun(olfun,var,body) ->
      let (newlfun,lvar,lval)=head_with_value (var,largs) in
      if lvar=[] then
	let v = val_interp { ist with lfun=newlfun@olfun } gl body in
        if lval=[] then locate_tactic_call loc v
	else interp_app ist gl v lval loc
      else
        VFun(newlfun@olfun,lvar,body)
    | _ ->
	user_err_loc (loc, "Tacinterp.interp_app",
          (str"Illegal tactic application"))

(* Gives the tactic corresponding to the tactic value *)
and tactic_of_value vle g =
  match vle with
  | VRTactic res -> res
  | VTactic (loc,tac) -> catch_error loc tac g
  | VFun _ -> error "A fully applied tactic is expected"
  | _ -> raise NotTactic

(* Evaluation with FailError catching *)
and eval_with_fail ist tac goal =
  try
    (match val_interp ist goal tac with
    | VTactic (loc,tac) -> VRTactic (catch_error loc tac goal)
    | a -> a)
  with
    | Stdpp.Exc_located (_,FailError (0,s)) | FailError (0,s) ->
	raise (Eval_fail s)
    | Stdpp.Exc_located (s',FailError (lvl,s)) ->
	raise (Stdpp.Exc_located (s',FailError (lvl - 1, s)))
    | FailError (lvl,s) ->
	raise (FailError (lvl - 1, s))

(* Interprets recursive expressions *)
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)) ->
                          (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 } gl u
  end

(* Interprets the clauses of a LetIn *)
and interp_letin ist gl = function
  | [] -> []
  | ((loc,id),None,t)::tl -> 
      let v = interp_tacarg ist gl t in
      check_is_value v;
      (id,v):: (interp_letin ist gl tl)
  | ((loc,id),Some com,tce)::tl ->
    let typ = interp_may_eval pf_interp_constr ist gl com
    and v = interp_tacarg 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.interp_letin"
          (str "Term or fully applied tactic expected in Let")
    in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)

(* Interprets the clauses of a LetCut *)
and letcut_interp ist = function 
  | [] -> tclIDTAC
  | (id,c,tce)::tl -> fun gl ->
    let typ = interp_constr_may_eval ist gl c
    and v = interp_tacarg 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.interp_letin"
          (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

(* Interprets the Match Context expressions *)
and match_context_interp ist g lr lmr =
  let rec apply_goal_sub ist env 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 {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch}
          mt goal
      else
        apply_hyps_context ist env goal mt lgoal mhyps hyps
    with
    | e when is_failure e -> raise e
    | NextOccurrence _ -> raise No_match
    | e when is_match_catchable e ->
      apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
  let rec apply_match_context ist env goal nrs lex lpt = 
    begin
    if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
    match lpt with
    | (All t)::tl ->
      begin
        db_mc_pattern_success ist.debug;
        try eval_with_fail ist t goal
         with e when is_match_catchable e ->
           apply_match_context ist env goal (nrs+1) (List.tl lex) tl
      end
    | (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 (pf_env goal) concl;
            if mhyps = [] then
            begin
              db_mc_pattern_success ist.debug;
              eval_with_fail {ist with lmatch=lgoal@ist.lmatch} mt goal
            end
            else
              apply_hyps_context ist env goal mt lgoal mhyps hyps
            end)
        with 
        | e when is_match_catchable e ->
          begin 
            (match e with
            | No_match -> db_matching_failure ist.debug
            | Eval_fail s -> db_eval_failure ist.debug s
            | _ -> db_logic_failure ist.debug e);
            apply_match_context ist env goal (nrs+1) (List.tl lex) tl
          end)
      |	Subterm (id,mg) ->
        (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
         with e when is_match_catchable e ->
           apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
    | _ ->
      errorlabstrm "Tacinterp.apply_match_context" (str
        "No matching clauses for Match Context")
        (v 0 (str "No matching clauses for Match Context" ++
        (if ist.debug=DebugOff then
           fnl() ++ str "(use \"Debug On\" for more info)"
         else mt())))
    end in
  let env = pf_env g in
  apply_match_context ist env g 0 lmr
    (read_match_rule (project g) env (fst (constr_list ist env)) lmr)

(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
  let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp
    lhyps_rest noccopt =
    match mhyps with
      | hd::tl ->
        let (lid,lc,lm,newlhyps,hyp_match,noccopt) =
          apply_one_mhyp_context ist env goal lmatch hd lhyps_mhyp noccopt in
        begin
          db_matched_hyp ist.debug (pf_env goal) hyp_match
                         (get_id_pattern lid);
          (try
          if tl = [] then
          begin
            db_mc_pattern_success ist.debug;
            eval_with_fail {ist with lfun=lfun@lid@lc@ist.lfun;
                                     lmatch=lmatch@lm@ist.lmatch} mt goal
          end
          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
              (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
           with
           | e when is_failure e -> raise e
	   | e when is_match_catchable e -> 
             (match noccopt with
             | None ->
               apply_hyps_context_rec ist mt lfun
                 lmatch mhyps newlhyps lhyps_rest None
             | Some nocc ->
               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 ist mt [] lgmatch mhyps hyps hyps None

  (* Interprets extended tactic generic arguments *)
and interp_genarg ist goal x =
  match genarg_tag x with
  | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x)
  | IntArgType -> in_gen wit_int (out_gen globwit_int x)
  | IntOrVarArgType ->
      let f = function
	| ArgVar locid -> eval_integer ist.lfun locid
	| ArgArg n as x -> x in
      in_gen wit_int_or_var (f (out_gen globwit_int_or_var x))
  | StringArgType ->
      in_gen wit_string (out_gen globwit_string x)
  | PreIdentArgType ->
      in_gen wit_pre_ident (out_gen globwit_pre_ident x)
  | IdentArgType ->
      in_gen wit_ident (eval_ident ist (out_gen globwit_ident x))
  | RefArgType ->
      in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x))
  | SortArgType ->
      in_gen wit_sort
        (destSort 
	  (pf_interp_constr ist goal 
	    (RSort (dummy_loc,out_gen globwit_sort x), None)))
  | ConstrArgType ->
      in_gen wit_constr (pf_interp_constr ist goal (out_gen globwit_constr x))
  | ConstrMayEvalArgType ->
      in_gen wit_constr_may_eval (interp_constr_may_eval ist goal (out_gen globwit_constr_may_eval x))
  | QuantHypArgType ->
      in_gen wit_quant_hyp
        (interp_quantified_hypothesis ist goal (out_gen globwit_quant_hyp x))
  | RedExprArgType ->
      in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
  | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x)
  | CastedOpenConstrArgType ->
      in_gen wit_casted_open_constr 
        (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x))
  | ConstrWithBindingsArgType ->
      in_gen wit_constr_with_bindings
        (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
  | List0ArgType _ -> app_list0 (interp_genarg ist goal) x
  | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
  | OptArgType _ -> app_opt (interp_genarg ist goal) x
  | PairArgType _ -> app_pair (interp_genarg ist goal) (interp_genarg ist goal) x
  | ExtraArgType s -> lookup_interp_genarg s ist goal x

(* Interprets the Match expressions *)
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
      val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} g mt
    with | NextOccurrence _ -> raise No_match
  in
  let rec apply_match ist csr = function
    | (All t)::_ ->
        (try val_interp ist g t
         with e when is_match_catchable e -> apply_match ist csr [])
    | (Pat ([],Term c,mt))::tl ->
        (try
          val_interp
            { ist with lmatch=(apply_matching c csr)@ist.lmatch } g mt
         with 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)
    | _ ->
      errorlabstrm "Tacinterp.apply_match" (str
        "No matching clauses for Match") in
  let csr = interp_constr_may_eval ist g constr in
  let env = pf_env g in
  let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in
  apply_match ist csr ilr

(* Interprets tactic expressions : returns a "tactic" *)
and interp_tactic ist tac gl =
  try tactic_of_value (val_interp ist gl tac) gl
  with | NotTactic ->
    errorlabstrm "Tacinterp.interp_tactic" (str
      "Must be a command or must give a tactic value")

(* Interprets a primitive tactic *)
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 gl hyp)
  | TacIntroMove (ido,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 (pf_interp_casted_constr ist gl c)
  | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
  | TacElim (cb,cbo) ->
      h_elim (interp_constr_with_bindings ist gl cb)
                (option_app (interp_constr_with_bindings ist gl) cbo)
  | TacElimType c -> h_elim_type (pf_interp_constr ist gl c)
  | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
  | TacCaseType c -> h_case_type (pf_interp_constr ist gl c)
  | TacFix (idopt,n) -> h_fix (eval_opt_ident ist idopt) n
  | TacMutualFix (id,n,l) ->
      let f (id,n,c) = (eval_ident ist id,n,pf_interp_constr 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) = (eval_ident ist id,pf_interp_constr ist gl c) in
      h_mutual_cofix (eval_ident ist id) (List.map f l)
  | TacCut c -> h_cut (pf_interp_constr ist gl c)
  | TacTrueCut (ido,c) ->
      h_true_cut (eval_opt_ident ist ido) (pf_interp_constr ist gl c)
  | TacForward (b,na,c) ->
      h_forward b (eval_name ist na) (pf_interp_constr ist gl c)
  | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
  | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
  | TacLetTac (id,c,clp) ->
      let clp = check_clause_pattern ist gl clp in
      h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp
  | TacInstantiate (n,c) -> h_instantiate n (pf_interp_constr 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 (interp_hyp 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 gl h)
  | TacNewInduction (c,cbo,ids) ->
      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 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 gl h1 in
      let h2 = interp_quantified_hypothesis ist gl h2 in
      Elim.h_double_induction h1 h2
  | TacDecomposeAnd c -> Elim.h_decompose_and (pf_interp_constr ist gl c)
  | TacDecomposeOr c -> Elim.h_decompose_or (pf_interp_constr ist gl c)
  | TacDecompose (l,c) ->
      let l = List.map (interp_inductive_or_metanum ist) l in
      Elim.h_decompose l (pf_interp_constr ist gl c)
  | TacSpecialize (n,l) ->
      h_specialize n (interp_constr_with_bindings ist gl l)
  | TacLApply c -> h_lapply (pf_interp_constr ist gl c)

  (* Context management *)
  | TacClear l -> h_clear (List.map (interp_hyp_or_metanum ist gl) l)
  | TacClearBody l -> h_clear_body (List.map (interp_hyp_or_metanum ist gl) l)
  | TacMove (dep,id1,id2) ->
      h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
  | TacRename (id1,id2) ->
      h_rename (interp_hyp ist gl id1) (eval_ident ist (snd id2))

  (* Constructors *)
  | TacLeft bl -> h_left (interp_bindings ist gl bl)
  | TacRight bl -> h_right (interp_bindings ist gl bl)
  | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
  | TacAnyConstructor t ->
      abstract_tactic (TacAnyConstructor t)
        (Tactics.any_constructor (option_app (interp_tactic ist) t))
  | TacConstructor (n,bl) ->
      h_constructor (skip_metaid n) (interp_bindings ist gl bl)

  (* Conversion *)
  | TacReduce (r,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 (pf_interp_pattern ist gl) occl)
        (pf_interp_constr ist gl c) (List.map (interp_hyp_location ist gl) cl)

  (* Equivalence relations *)
  | TacReflexivity -> h_reflexivity
  | TacSymmetry -> h_symmetry
  | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)

  (* For extensions *)
  | TacExtend (loc,opn,l) ->
      fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl
  | TacAlias (_,l,body) -> fun gl ->
    let f x = match genarg_tag x with
    | IdentArgType -> 
	let id = out_gen globwit_ident x in
	(try VConstr (mkVar (eval_variable ist gl (dummy_loc,id)))
	 with Not_found -> VIdentifier id)
    | RefArgType -> 
        VConstr (constr_of_reference 
          (pf_interp_reference ist gl (out_gen globwit_ref x)))
    | ConstrArgType ->
        VConstr (pf_interp_constr ist gl (out_gen globwit_constr x))
    | ConstrMayEvalArgType ->
      VConstr
        (interp_constr_may_eval ist gl (out_gen globwit_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

(* Initial call for interpretation *)
let interp_tac_gen lfun lmatch debug t gl = 
  interp_tactic { lfun=lfun; lmatch=lmatch; debug=debug } 
    (intern_tactic {
      ltacvars = (List.map fst lfun, []); ltacrecvars = [];
      metavars = List.map fst lmatch;
      gsigma = project gl; genv = pf_env gl } t) gl

let eval_tactic t = interp_tactic { lfun=[]; lmatch=[]; debug=get_debug() } t

let interp t = interp_tac_gen [] [] (get_debug()) t

(* Hides interpretation for pretty-print *)
let hide_interp t ot gl =
  let ist = { ltacvars = ([],[]); ltacrecvars = []; metavars = [];
            gsigma = project gl; genv = pf_env gl } in
  let te = intern_tactic ist t in
  let t = eval_tactic te in
  match ot with 
  | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
  | Some t' -> abstract_tactic_expr (TacArg (Tacexp te)) (tclTHEN t t') gl

(***************************************************************************)
(* Substitution at module closing time *)

let subst_quantified_hypothesis _ x = x

let subst_inductive subst (kn,i) = (subst_kn subst kn,i)

let subst_rawconstr subst (c,e) =
  assert (e=None); (* e<>None only for toplevel tactics *)
  (subst_raw subst c,None)

let subst_binding subst (loc,b,c) =
  (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c)

let subst_bindings subst = function
  | NoBindings -> NoBindings
  | ImplicitBindings l -> ImplicitBindings (List.map (subst_rawconstr subst) l)
  | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l)

let subst_raw_with_bindings subst (c,bl) =
  (subst_rawconstr subst c, subst_bindings subst bl)

let subst_induction_arg subst = function
  | ElimOnConstr c -> ElimOnConstr (subst_rawconstr subst c)
  | ElimOnAnonHyp n as x -> x
  | ElimOnIdent id as x -> x

let subst_evaluable_reference subst = function
  | EvalVarRef id -> EvalVarRef id
  | EvalConstRef kn -> EvalConstRef (subst_kn subst kn)

let subst_and_short_name f (c,n) =
  assert (n=None); (* since tacdef are strictly globalized *)
  (f c,None)

let subst_or_metanum f =  function
  | AN x -> AN (f x)
  | MetaNum (_loc,n) -> MetaNum (loc,n)

let subst_or_var f =  function
  | ArgVar _ as x -> x
  | ArgArg (x) -> ArgArg (f x)

let subst_located f (_loc,id) = (loc,f id)

let subst_reference subst r = (* TODO: subst ltac global names *) r

let subst_global_reference subst = 
  subst_or_var (subst_located (subst_global subst))

let subst_evaluable subst =
  subst_or_metanum (subst_or_var
    (subst_and_short_name (subst_evaluable_reference subst)))

let subst_unfold subst (l,e) = 
  (l,subst_evaluable subst e)

let subst_flag subst red =
  { red with rConst = List.map (subst_evaluable subst) red.rConst }

let subst_constr_occurrence subst (l,c) = (l,subst_rawconstr subst c)

let subst_redexp subst = function
  | Unfold l -> Unfold (List.map (subst_unfold subst) l)
  | Fold l -> Fold (List.map (subst_rawconstr subst) l)
  | Cbv f -> Cbv (subst_flag subst f)
  | Lazy f -> Lazy (subst_flag subst f)
  | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
  | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
  | (Red _ | Hnf as r) -> r
  | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c)

let subst_raw_may_eval subst = function
  | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c)
  | ConstrContext (locid,c) -> ConstrContext (locid,subst_rawconstr subst c)
  | ConstrTypeOf c -> ConstrTypeOf (subst_rawconstr subst c)
  | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)

let subst_match_pattern subst = function
  | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc)
  | Term pc -> Term (subst_pattern subst pc)

let rec subst_match_context_hyps subst = function
  | NoHypId mp :: tl ->
      NoHypId (subst_match_pattern subst mp)
      :: subst_match_context_hyps subst tl
  | Hyp (locs,mp) :: tl ->
      Hyp (locs,subst_match_pattern subst mp)
      :: subst_match_context_hyps subst tl
  | [] -> []

let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
  (* Basic tactics *)
  | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
  | TacAssumption as x -> x
  | TacExact c -> TacExact (subst_rawconstr subst c)
  | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
  | TacElim (cb,cbo) ->
      TacElim (subst_raw_with_bindings subst cb,
               option_app (subst_raw_with_bindings subst) cbo)
  | TacElimType c -> TacElimType (subst_rawconstr subst c)
  | TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
  | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
  | TacFix (idopt,n) as x -> x
  | TacMutualFix (id,n,l) ->
      TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
  | TacCofix idopt as x -> x
  | TacMutualCofix (id,l) ->
      TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
  | TacCut c -> TacCut (subst_rawconstr subst c)
  | TacTrueCut (ido,c) -> TacTrueCut (ido, subst_rawconstr subst c)
  | TacForward (b,na,c) -> TacForward (b,na,subst_rawconstr subst c)
  | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
  | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
  | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
  | TacInstantiate (n,c) -> TacInstantiate (n,subst_rawconstr subst c)

  (* Automation tactics *)
  | TacTrivial l -> TacTrivial l
  | TacAuto (n,l) -> TacAuto (n,l)
  | TacAutoTDB n -> TacAutoTDB n
  | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
  | TacDestructConcl -> TacDestructConcl
  | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
  | TacDAuto (n,p) -> TacDAuto (n,p)

  (* Derived basic tactics *)
  | TacOldInduction h as x -> x
  | TacNewInduction (c,cbo,ids) ->
      TacNewInduction (subst_induction_arg subst c,
               option_app (subst_raw_with_bindings subst) cbo, ids)
  | TacOldDestruct h as x -> x
  | TacNewDestruct (c,cbo,ids) ->
      TacNewDestruct (subst_induction_arg subst c,
               option_app (subst_raw_with_bindings subst) cbo, ids)
  | TacDoubleInduction (h1,h2) as x -> x
  | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
  | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
  | TacDecompose (l,c) ->
      let l = 
        List.map (subst_or_metanum (subst_or_var (subst_inductive subst))) l in
      TacDecompose (l,subst_rawconstr subst c)
  | TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l)
  | TacLApply c -> TacLApply (subst_rawconstr subst c)

  (* Context management *)
  | TacClear l as x -> x
  | TacClearBody l as x -> x
  | TacMove (dep,id1,id2) as x -> x
  | TacRename (id1,id2) as x -> x

  (* Constructors *)
  | TacLeft bl -> TacLeft (subst_bindings subst bl)
  | TacRight bl -> TacRight (subst_bindings subst bl)
  | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
  | TacAnyConstructor t -> TacAnyConstructor (option_app (subst_tactic subst) t)
  | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)

  (* Conversion *)
  | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
  | TacChange (occl,c,cl) ->
      TacChange (option_app (subst_constr_occurrence subst) occl,
        subst_rawconstr subst c, cl)

  (* Equivalence relations *)
  | TacReflexivity | TacSymmetry as x -> x
  | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)

  (* For extensions *)
  | TacExtend (_loc,opn,l) ->
      let _ = lookup_tactic opn in
      TacExtend (loc,opn,List.map (subst_genarg subst) l)
  | TacAlias (s,l,body) ->
      TacAlias (s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,subst_tactic subst body)

and subst_tactic subst (t:glob_tactic_expr) = match t with
  | TacAtom (_loc,t) -> TacAtom (loc, subst_atomic subst t)
  | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
  | TacLetRecIn (lrc,u) ->
      let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
      TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
  | TacLetIn (l,u) ->
      let l = List.map (fun (n,c,b) -> (n,option_app (subst_raw_may_eval subst) c,subst_tacarg subst b)) l in
      TacLetIn (l,subst_tactic subst u)
  | TacLetCut l ->
      let f (n,c,t) = (n,subst_raw_may_eval subst c,subst_tacarg subst t) in
      TacLetCut (List.map f l)
  | TacMatchContext (lr,lmr) ->
      TacMatchContext(lr, subst_match_rule subst lmr)
  | TacMatch (c,lmr) ->
      TacMatch (subst_raw_may_eval subst c,subst_match_rule subst lmr)
  | TacId | TacFail _ as x -> x
  | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
  | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
  | TacThen (t1,t2) ->
      TacThen (subst_tactic subst t1,subst_tactic subst t2)
  | TacThens (t,tl) ->
      TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
  | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
  | TacTry tac -> TacTry (subst_tactic subst tac)
  | TacInfo tac -> TacInfo (subst_tactic subst tac)
  | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
  | TacOrelse (tac1,tac2) ->
      TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
  | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
  | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
  | TacArg a -> TacArg (subst_tacarg subst a)

and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)

and subst_tacarg subst = function
  | TacVoid -> TacVoid
  | Reference r -> Reference (subst_or_var (subst_reference subst) r)
  | Identifier id -> Identifier id
  | Integer n -> Integer n
  | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
  | MetaIdArg (_loc,_) -> error_syntactic_metavariables_not_allowed loc
  | TacCall (_loc,f,l) ->
      TacCall (_loc,
        subst_or_var (subst_reference subst) f,
	List.map (subst_tacarg subst) l)
  | Tacexp t -> Tacexp (subst_tactic subst t)
  | TacDynamic(_,t) as x ->
      (match tag t with
	| "tactic" | "value" | "constr" -> x
	| s -> anomaly_loc (loc, "Tacinterp.val_interp",
                 str "Unknown dynamic: <" ++ str s ++ str ">"))

(* Reads the rules of a Match Context or a Match *)
and subst_match_rule subst = function
  | (All tc)::tl ->
      (All (subst_tactic subst tc))::(subst_match_rule subst tl)
  | (Pat (rl,mp,tc))::tl ->
      let hyps = subst_match_context_hyps subst rl in
      let pat = subst_match_pattern subst mp in
      Pat (hyps,pat,subst_tactic subst tc)
      ::(subst_match_rule subst tl)
  | [] -> []

and subst_genarg subst (x:glob_generic_argument) =
  match genarg_tag x with
  | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x)
  | IntArgType -> in_gen globwit_int (out_gen globwit_int x)
  | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
  | StringArgType -> in_gen globwit_string (out_gen globwit_string x)
  | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
  | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x)
  | RefArgType ->
      in_gen globwit_ref (subst_global_reference subst 
	(out_gen globwit_ref x))
  | SortArgType ->
      in_gen globwit_sort (out_gen globwit_sort x)
  | ConstrArgType ->
      in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x))
  | ConstrMayEvalArgType ->
      in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
  | QuantHypArgType ->
      in_gen globwit_quant_hyp
        (subst_quantified_hypothesis subst (out_gen globwit_quant_hyp x))
  | RedExprArgType ->
      in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
  | TacticArgType ->
      in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x))
  | CastedOpenConstrArgType ->
      in_gen globwit_casted_open_constr 
        (subst_rawconstr subst (out_gen globwit_casted_open_constr x))
  | ConstrWithBindingsArgType ->
      in_gen globwit_constr_with_bindings
        (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
  | List0ArgType _ -> app_list0 (subst_genarg subst) x
  | List1ArgType _ -> app_list1 (subst_genarg subst) x
  | OptArgType _ -> app_opt (subst_genarg subst) x
  | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
  | ExtraArgType s -> lookup_genarg_subst s subst x

(***************************************************************************)
(* Tactic registration *)

(* For bad tactic calls *)
let bad_tactic_args s =
  anomalylabstrm s
    (str "Tactic " ++ str s ++ str " called with bad arguments")

(* Declaration of the TAC-DEFINITION object *)
let add (sp,td) = mactab := Gmap.add sp td !mactab

let register_tacdef (sp,td) = sp,td

let cache_md (_,defs) =
  (* Needs a rollback if something goes wrong *)
  List.iter (fun (sp,_) -> Nametab.push_tactic (Until 1) sp) defs;
  List.iter add (List.map register_tacdef defs)

let subst_md (_,subst,defs) =
  List.map (fun (sp,t) -> (sp,subst_tactic subst t)) defs

let (inMD,outMD) =
  declare_object {(default_object "TAC-DEFINITION") with
     cache_function  = cache_md;
     open_function   = (fun i o -> if i=1 then cache_md o);
     subst_function = subst_md;
     classify_function = (fun (_,o) -> Substitute o);       
     export_function = (fun x -> Some x)}

(* Adds a definition for tactics in the table *)
let make_absolute_name (loc,id) =
  let sp = Lib.make_path id in
  if Gmap.mem sp !mactab then
    errorlabstrm "Tacinterp.add_tacdef" 
      (str "There is already a Meta Definition or a Tactic Definition named "
       ++ pr_sp sp);
  sp

let make_empty_glob_sign () =
  { ltacvars = ([],[]); ltacrecvars = [];
    metavars = []; gsigma = Evd.empty; genv = Global.env() }

let add_tacdef isrec tacl =
  let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
  let ist =
    {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in
  let gtacl =
    List.map2 (fun (_,sp) (_,def) ->
        (sp,Options.with_option strict_check (intern_tactic ist) def))
      rfun tacl in
  let id0 = fst (List.hd rfun) in
  let _ = Lib.add_leaf id0 (inMD gtacl) in
  List.iter
    (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
    rfun

(***************************************************************************)
(* Other entry points *)

let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x

let interp_redexp env evc r = 
  let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in
  let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = evc } in
  redexp_interp ist evc env (intern_redexp gist r)

(***************************************************************************)
(* Backwarding recursive needs of tactic glob/interp/eval functions *)

let _ = Auto.set_extern_interp
  (fun l -> interp_tactic {lfun=[];lmatch=l;debug=get_debug()})
let _ = Auto.set_extern_intern_tac 
  (fun l -> intern_tactic {(make_empty_glob_sign()) with metavars=l})
let _ = Auto.set_extern_subst_tactic subst_tactic
let _ = Dhyp.set_extern_interp eval_tactic
let _ = Dhyp.set_extern_intern_tac
  (fun t -> intern_tactic (make_empty_glob_sign()) t)