-prerr_endline ("<MY_CUT: " ^ CicPp.ppterm a ^ " <=> " ^ CicPp.ppterm b) ;
-prerr_endline ("### IN MY_CUT: ") ;
-prerr_endline ("@ " ^ CicPp.ppterm ty) ;
-List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ;
-prerr_endline ("##- IN MY_CUT ") ;
-let res =
- let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
-(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *)
- PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status
-in
-prerr_endline "EUREKA" ;
-res
+ let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
+ let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let irl =
+ ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+ let (proof,goals) =
+ rewrite_tac ~term:(C.Meta (fresh_meta,irl))
+ ~status:((curi,metasenv',pbo,pty),goal)
+ in
+ (proof,fresh_meta::goals)