From 0579efd93eebb18f94c90718b092ae4b68a2262d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 2 Oct 2018 08:18:34 +0200
Subject: Fix deprecation warnings.

---
 src/tac2entries.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index c26fbdc478..95a5f954c6 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -750,14 +750,14 @@ let perform_eval e =
       Proof_global.give_me_the_proof ()
     with Proof_global.NoCurrentProof ->
       let sigma = Evd.from_env env in
-      Vernacexpr.SelectAll, Proof.start sigma []
+      Goal_select.SelectAll, Proof.start sigma []
   in
   let v = match selector with
-  | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i v
-  | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l v
-  | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id v
-  | Vernacexpr.SelectAll -> v
-  | Vernacexpr.SelectAlreadyFocused -> assert false (** TODO **)
+  | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
+  | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
+  | Goal_select.SelectId id -> Proofview.tclFOCUSID id v
+  | Goal_select.SelectAll -> v
+  | Goal_select.SelectAlreadyFocused -> assert false (** TODO **)
   in
   (** HACK: the API doesn't allow to return a value *)
   let ans = ref None in
-- 
cgit v1.2.3