-let equality_replace a b ~status =
-debug("inizio EQ\n");
- let module C = Cic in
- let proof,goal = status in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
- let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
-debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
- let (proof,goals) =
- EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
- ~status:((curi,metasenv',pbo,pty),goal)
- in
- let new_goals = fresh_meta::goals in
-debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
- ^string_of_int( List.length goals)^"+ meta\n");
- (proof,new_goals)
+let equality_replace a b =
+ let equality_replace a b status =
+ debug("inizio EQ\n");
+ let module C = Cic in
+ let proof,goal = status in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+ debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
+ let (proof,goals) = apply_tactic
+ (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)))
+ ((curi,metasenv',pbo,pty),goal)
+ in
+ let new_goals = fresh_meta::goals in
+ debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
+ ^string_of_int( List.length goals)^"+ meta\n");
+ (proof,new_goals)
+ in
+ mk_tactic (equality_replace a b)