+ | TacticAst.LetIn (loc,term,name) ->
+ Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
+ | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
+ ProofEngineTypes.mk_tactic
+ (fun (((_,metasenv,_,_),goal) as status) ->
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let where, also_in_hypotheses =
+ if ident = "goal" then
+ ty, false
+ else
+ let hyp =
+ try
+ List.find (function
+ | Some (Cic.Name name,entry) when name = ident -> true
+ | _ -> false)
+ context
+ with
+ Not_found ->
+ raise (ProofEngineTypes.Fail
+ (ident ^ " is not an hypothesis"))
+ in
+ (match hyp with
+ | Some (_, Cic.Decl term) -> term
+ | Some (_, Cic.Def (term,ty)) -> term
+ | None -> assert false),true
+ in
+ let pointers = CicUtil.select ~term:where ~context:path in
+ (match reduction_kind with
+ | `Normalize ->
+ ProofEngineTypes.apply_tactic
+ (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
+ status
+ | `Reduce ->
+ ProofEngineTypes.apply_tactic
+ (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
+ status
+ | `Simpl ->
+ ProofEngineTypes.apply_tactic
+ (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
+ status
+ | `Whd ->
+ ProofEngineTypes.apply_tactic
+ (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
+ status))
+ | TacticAst.Reduce (_,reduction_kind,opts) ->
+ let terms, also_in_hypotheses =
+ match opts with
+ | Some (l,`Goal) -> Some l, false
+ | Some (l,`Everywhere) -> Some l, true
+ | None -> None, false
+ in
+ (match reduction_kind with
+ | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
+ | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
+ | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
+ | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
+ | TacticAst.Rewrite (_,dir,t,ident) ->
+ if dir = `Left then
+ EqualityTactics.rewrite_tac ~term:t
+ else
+ EqualityTactics.rewrite_back_tac ~term:t