diff options
| author | Pierre-Marie Pédrot | 2016-05-17 22:37:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 22:38:40 +0200 |
| commit | f7fb1918619fcef384d4aa84938246de67c707fa (patch) | |
| tree | 6f8b1b8ba71681b06b4a74ddeee76d02a3ef09dd /tactics/equality.ml | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
| parent | dadd4003b6607ccc103658f842b5efbd6d8ab57f (diff) | |
Putting all the tactics exported by the Tactics module in the new monad API.
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index cb1d82ae6b..12d31d0f31 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -79,8 +79,6 @@ let _ = (* Rewriting tactics *) -let clear ids = Proofview.V82.tactic (clear ids) - let tclNOTSAMEGOAL tac = Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac)) @@ -976,7 +974,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1318,7 +1316,7 @@ let inject_if_homogenous_dependent_pair ty = onLastHyp (fun hyp -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar hyp]; - Proofview.V82.tactic (refine + Proofview.V82.tactic (Tacmach.refine (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> @@ -1364,7 +1362,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (refine pf)]) + Proofview.V82.tactic (Tacmach.refine pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) @@ -1584,7 +1582,7 @@ let substClause l2r c cls = Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) - [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)] + [Proofview.tclUNIT (); exact_no_check c] end } let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) |