diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-15 16:38:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-16 10:06:30 +0200 |
| commit | 4f6fd16c06b9e11bc2619a34c1629bd71aba76de (patch) | |
| tree | 3ab43f96dc31eb792bb41ca8d26cf4114511b840 /plugins/ssr | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
Remove the last use of the low-level Proof_type API in ssr.
Diffstat (limited to 'plugins/ssr')
| -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 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 |