Removing the globTacticIn primitive.

It was not used in Coq codebase, and the only known user was ssreflect up
to commit 95354e0dee.

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))
@@ -2386,11 +2380,6 @@ let interp_redexp env sigma r =
   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 *)
 
 let _ =
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"