* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
+
+(* $Id$ *)
let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
| _::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
- let dummy = "dummy" in
+ let dummy = "dummy" in
Some arg,false,
(fun ~term typ ->
Tacticals.seq
ty_of_with_what ty_of_t_in_context u in
if b then
let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
- let pattern_for_t = None,[],concl_pat_for_t in
+ let pattern_for_t = None,[],Some concl_pat_for_t in
t_in_context,pattern_for_t
else
raise
~continuations:[
T.then_
~start:(
- rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
+ rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
~continuation:(
T.then_
~start:(