aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 490ded9d4..ded9fa66b 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -960,7 +960,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
| _ -> assert false
in loop sigma t [] n in
pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t));
- Refiner.refiner (Proof_type.Refine (EConstr.Unsafe.to_constr t)) gl
+ Tacmach.refine_no_check (EConstr.Unsafe.to_constr t) gl
let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in