* 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