From d54cfa6a006002cafeee3aca684dcca5e88edb39 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Mon, 1 Oct 2018 14:28:33 +0200
Subject: fix deprecation warnings

---
 tuto3/src/tuto_tactic.ml | 4 ++--
 1 file 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
-- 
cgit v1.2.3