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 /plugins | |
| parent | f499083e65ba629e0232fad3f3bbc7fe21d9da2f (diff) | |
Remove Refiner.refiner.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 2151ad7873..9b578d4697 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -43,7 +43,7 @@ let finish_proof dynamic_infos g = let refine c = Proofview.V82.of_tactic - (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)) + (Logic.refiner ~check:true EConstr.Unsafe.(to_constr c)) let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 01e8daf82d..5c25db1a82 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1029,7 +1029,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t = pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Proofview.(V82.of_tactic (Tacticals.New.tclTHENLIST [ - Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t); + Logic.refiner ~check:false EConstr.Unsafe.(to_constr t); (if first_goes_last then cycle 1 else tclUNIT ()) ])) gl end diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 8e75ba7a2b..a12b4aad11 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -482,7 +482,7 @@ let revtoptac n0 = let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) + Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) end let equality_inj l b id c = |