diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:36:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:16:21 +0200 |
| commit | e5b355107d985d7efe2976b9eee9b6c182e25f24 (patch) | |
| tree | f17d55f201d22a067688524dab2f56f7d2f5ef8a /tactics | |
| parent | f499083e65ba629e0232fad3f3bbc7fe21d9da2f (diff) | |
Remove Refiner.refiner.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 39017c946f..3aa7626aaa 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1047,7 +1047,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) - [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] + [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1366,7 +1366,7 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + Logic.refiner ~check:true EConstr.Unsafe.(to_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> @@ -1412,7 +1412,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; - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)]) + Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3133f9be1e..eb7f2190a8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1383,7 +1383,7 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = if not with_evars && occur_meta clenv.evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in + let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN |