From 6cc40e73879aec50227c9576100a381cc11ade30 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Nov 2018 13:55:14 +0100
Subject: [warnings] Fix couple of warnings related to API..

Changes in declare following @SkySkimmer's advice.
---
 tuto1/src/simple_declare.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tuto1/src')

diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index af4dd5bddf..50fd170663 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -1,10 +1,10 @@
+(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
 let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
-  let open EConstr in
   let sigma = Evd.minimize_universes sigma in
-  let body = to_constr sigma body in
-  let tyopt = Option.map (to_constr sigma) tyopt in
+  let body = EConstr.to_constr sigma body in
+  let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
   let uvars_fold uvars c =
-    Univ.LSet.union uvars (Univops.universes_of_constr c) in
+    Univ.LSet.union uvars (Vars.universes_of_constr c) in
   let uvars = List.fold_left uvars_fold Univ.LSet.empty
      (Option.List.cons tyopt [body]) in
   let sigma = Evd.restrict_universe_context sigma uvars in
-- 
cgit v1.2.3