From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:26:21 +0200 Subject: Split off Universes functions dealing with generating new universes. --- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrequality.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/ssr') 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 7d7655d29..a31022919 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -435,7 +435,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 @@ -482,7 +482,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 -- cgit v1.2.3