diff options
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |