diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 5 |
4 files changed, 6 insertions, 9 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e9e045a53..c0026616d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1221,7 +1221,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) + (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index eadc6d218..f929e9430 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -438,7 +438,7 @@ let lz_setoid_relation = | env', srel when env' == env -> srel | _ -> let srel = - try Some (Universes.constr_of_global @@ + try Some (UnivGen.constr_of_global @@ Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation") with _ -> None in last_srel := (env, srel); srel @@ -485,7 +485,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 6e17e8e15..c6beb08c5 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -184,9 +184,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) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 9cc4f5cec..937e68b06 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -32,9 +32,8 @@ let get_index = function ArgArg i -> i | _ -> let tclPERM perm tac gls = let subgls = tac gls in - let sigma, subgll = Refiner.unpackage subgls in - let subgll' = perm subgll in - Refiner.repackage sigma subgll' + let subgll' = perm subgls.Evd.it in + re_sig subgll' subgls.Evd.sigma let rot_hyps dir i hyps = let n = List.length hyps in |