From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 plugins/ltac/tacintern.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'plugins/ltac/tacintern.ml')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e9..75227def0f 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function
       GRef (loc,locate_global_with_alias lqid,None), 
 	if strict then None else Some (CRef (r,None))
 
-let intern_move_location ist = function
-  | MoveAfter id -> MoveAfter (intern_hyp ist id)
-  | MoveBefore id -> MoveBefore (intern_hyp ist id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
-- 
cgit v1.2.3