+ let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
+ match hyps_pat with
+ he::(_::_ as tl) ->
+ PET.apply_tactic
+ (Tacticals.then_
+ (rewrite_tac ~direction
+ ~pattern:(None,[he],None) equality)
+ (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality)
+ ) status
+ | [_] as hyps_pat when concl_pat <> None ->
+ PET.apply_tactic
+ (Tacticals.then_
+ (rewrite_tac ~direction
+ ~pattern:(None,hyps_pat,None) equality)
+ (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
+ ) status
+ | _ ->