adapts to master on Oct. 1st 2018, but warnings remain

4 files changed, 9 insertions, 10 deletions

diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index b152583824..e171688083 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -21,10 +21,10 @@ END
 
 VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
 | [ "HelloAgain" reference(r)] ->
-(* The function Libnames.pr_reference was found by searching all mli files
-   for a function of type reference -> Pp.t *)
+(* The function Ppconstr.pr_qualid was found by searching all mli files
+   for a function of type qualid -> Pp.t *)
   [ Feedback.msg_notice
-      (strbrk "Hello again " ++ Libnames.pr_reference r)]
+      (strbrk "Hello again " ++ Ppconstr.pr_qualid r)]
 END
 
 (* According to parsing/pcoq.mli, e has type constr_expr *)
@@ -132,7 +132,7 @@ END
 
 TACTIC EXTEND my_intro
 | [ "my_intro" ident(i) ] ->
-  [ Tactics.introduction ~check:false i]
+  [ Tactics.introduction i]
 END
 
 (* if one write this:
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 5fd0b2e84b..10fa640548 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -1,11 +1,10 @@
 let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
   let open EConstr in
-  let env = Global.env () 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 uvars_fold uvars c =
-    Univ.LSet.union uvars (Univops.universes_of_constr env c) in
+    Univ.LSet.union uvars (Univops.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
@@ -19,8 +18,8 @@ let packed_declare_definition ident value_with_constraints =
   let sigma = Evd.from_ctx ctx in
   let k = (Decl_kinds.Global,
            Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
-  let udecl = Univdecls.default_univ_decl in
+  let udecl = UState.default_univ_decl in
   let nohook = Lemmas.mk_hook (fun _ x -> x) in
   ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
 
-(* But this definition cannot be undone by Reset ident *)
\ No newline at end of file
+(* But this definition cannot be undone by Reset ident *)
diff --git a/tuto1/src/simple_print.mli b/tuto1/src/simple_print.mli
index c59316e84b..254b56ff79 100644
--- a/tuto1/src/simple_print.mli
+++ b/tuto1/src/simple_print.mli
@@ -1 +1 @@
-val simple_body_access : Globnames.global_reference -> Constr.constr
+val simple_body_access : Names.GlobRef.t -> Constr.constr
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index fbb6863f7e..3e926ad7f2 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -9,7 +9,7 @@ let collect_constants () =
   if (!constants = []) then
     let open Coqlib in
     let open EConstr in
-    let open Universes in
+    let open UnivGen in
     let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in
     let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in
     let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in