- | 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