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.

---
 tactics/autorewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/autorewrite.ml')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c3857e6b8b..627ac31f50 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
   let try_rewrite dir ctx c tc =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+    let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-- 
cgit v1.2.3