Merge pull request #17 from ejgallego/fix_warn

[warnings] Fix couple of warnings related to API..

1 files changed, 4 insertions, 4 deletions

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