fix deprecation warnings

1 files changed, 2 insertions, 2 deletions

diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index 3e926ad7f2..708b9c1877 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -56,7 +56,7 @@ let package i = Goal.enter begin fun gl ->
    [(* this means that the applied theorem is not to be cleared. *)
     None, (CAst.make (c_M (),
            (* we don't specialize the theorem with extra values. *)
-           Misctypes.NoBindings))]
+           Tactypes.NoBindings))]
      (* we don't destruct the result according to any intro_pattern *)
     None
   end
@@ -140,5 +140,5 @@ let pack_tactic i =
       else
         tclTHEN (package i)
           (tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
-             (Tactics.move_hyp h_hyps_id Misctypes.MoveLast))
+             (Tactics.move_hyp h_hyps_id Logic.MoveLast))
     end