+ let arg,dir2,tac,concl_pat,gty =
+ match hyps_pat with
+ [] -> None,true,PT.exact_tac,concl_pat,gty
+ | [name,pat] ->
+ (*CSC: bug here; I am ignoring the concl_pat *)
+ let rec find_hyp n =
+ function
+ [] -> assert false
+ | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+ Cic.Rel n, CicSubstitution.lift n ty
+ | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet!*)
+ | _::tl -> find_hyp (n+1) tl
+ in
+ let arg,gty = find_hyp 1 context in
+ let last_hyp_name_of_status (proof,goal) =
+ let curi, metasenv, pbo, pty = proof in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+ match context with
+ (Some (Cic.Name s,_))::_ -> s
+ | _ -> assert false
+ in
+ Some arg,false,
+ (fun ~term ->
+ Tacticals.seq
+ ~tactics:
+ [PT.letin_tac term;
+ PET.mk_tactic (fun status ->
+ PET.apply_tactic
+ (ProofEngineStructuralRules.clearbody
+ (last_hyp_name_of_status status)) status);
+ PET.mk_tactic (fun status ->
+ let hyp = last_hyp_name_of_status status in
+ PET.apply_tactic
+ (ReductionTactics.simpl_tac
+ ~pattern:
+ (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None))
+ status);
+ ProofEngineStructuralRules.clear name;
+ PET.mk_tactic (fun status ->
+ let hyp = last_hyp_name_of_status status in
+ PET.apply_tactic
+ (ProofEngineStructuralRules.rename hyp name) status)
+ ]),
+ pat,gty
+ | _ -> assert false (*CSC: not implemented yet!*)
+ in
+ let if_right_to_left do_not_change a b =
+ match direction with
+ | `RightToLeft -> if do_not_change then a else b
+ | `LeftToRight -> if do_not_change then b else a
+ in