From 3e0643a4073c02767f44c0b77019a0e183e1e296 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Dec 2015 20:30:49 +0100
Subject: Removing the globTacticIn primitive.

It was not used in Coq codebase, and the only known user was ssreflect up
to commit 95354e0dee.
---
 tactics/tacintern.ml  |  2 +-
 tactics/tacinterp.ml  | 13 +------------
 tactics/tacinterp.mli |  1 -
 tactics/tacsubst.ml   |  2 +-
 4 files changed, 3 insertions(+), 15 deletions(-)

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 1778221b02..23e7b85a6c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -710,7 +710,7 @@ and intern_tacarg strict onlytac ist = function
     let (_, arg) = Genintern.generic_intern ist arg in
     TacGeneric arg
   | TacDynamic(loc,t) as x ->
-    if Dyn.has_tag t "tactic" || Dyn.has_tag t "value" then x
+    if Dyn.has_tag t "value" then x
     else if Dyn.has_tag t "constr" then
       if onlytac then error_tactic_expected loc else x
     else
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f1fd526082..922dc2bc41 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -212,10 +212,6 @@ let constr_of_id env id =
 
 (* To embed tactics *)
 
-let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t),
-     (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) =
-  Dyn.create "tactic"
-
 let ((value_in : value -> Dyn.t),
      (value_out : Dyn.t -> value)) = Dyn.create "value"
 
@@ -1459,9 +1455,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
   | Tacexp t -> val_interp ist t
   | TacDynamic(_,t) ->
       let tg = (Dyn.tag t) in
-      if String.equal tg "tactic" then
-        val_interp ist (tactic_out t ist)
-      else if String.equal tg "value" then
+      if String.equal tg "value" then
         Ftactic.return (value_out t)
       else if String.equal tg "constr" then
         Ftactic.return (Value.of_constr (constr_out t))
@@ -2385,11 +2379,6 @@ let interp_redexp env sigma r =
   let gist = { fully_empty_glob_sign with genv = env; } in
   interp_red_expr ist env sigma (intern_red_expr gist r)
 
-(***************************************************************************)
-(* Embed tactics in raw or glob tactic expr *)
-
-let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t))
-
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 60c9dc43e4..c7364ee62d 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -46,7 +46,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env ->
     a [constr]. *)
 
 (** To embed several objects in Coqast.t *)
-val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
 val valueIn : value -> raw_tactic_arg
 
 (** Sets the debugger mode *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index afffaffbe9..8e46e625f3 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -268,7 +268,7 @@ and subst_tacarg subst = function
   | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
   | TacDynamic(the_loc,t) as x ->
       (match Dyn.tag t with
-	| "tactic" | "value" -> x
+	| "value" -> x
         | "constr" ->
           TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
 	| s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
-- 
cgit v1.2.3