diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 01e8daf82d..5f463f8de4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0 (* }}} *) let pf_merge_uc uc gl = - re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc) + re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc) let pf_merge_uc_of sigma gl = let ucst = Evd.evar_universe_context sigma in pf_merge_uc ucst gl @@ -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 = |