* 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
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:(