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 ++++----
 tuto3/src/tuto_tactic.ml    | 2 +-
 2 files changed, 5 insertions(+), 5 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
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index cb73a4486b..9818867621 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -15,7 +15,7 @@ let collect_constants () =
     let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
     let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
     let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
-    constants := List.map (fun x -> of_constr (constr_of_global x))
+    constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x))
       [gr_H; gr_M; gr_R; gr_P; gr_U];
     !constants
   else
-- 
cgit v1.2.3