diff options
Diffstat (limited to 'plugins/ssr/ssrfwd.ml')
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index a5765feb..e367cd32 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -68,25 +68,18 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let inHaveTCResolution = Libobject.declare_object { - (Libobject.default_object "SSRHAVETCRESOLUTION") with - Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v); - Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v); - Libobject.classify_function = (fun v -> Libobject.Keep v); -} let _ = Goptions.declare_bool_option { Goptions.optname = "have type classes"; Goptions.optkey = ["SsrHave";"NoTCResolution"]; Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); Goptions.optdepr = false; - Goptions.optwrite = (fun b -> - Lib.add_anonymous_leaf (inHaveTCResolution b)) } + Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); + } open Constrexpr open Glob_term -open Misctypes let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) @@ -184,9 +177,7 @@ let havetac ist let gs = List.map (fun (_,a) -> Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in - let tacopen_skols gl = - let stuff, g = Refiner.unpackage gl in - Refiner.repackage stuff (gs @ [g]) in + let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in let gl, ty = pf_e_type_of gl t in gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id, Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac) |