Getting rid of the dynamic node of the tactic AST.

6 files changed, 6 insertions, 34 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 73130d380..ead221c5f 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,7 +209,6 @@ constraint 'a = <
 (** Possible arguments of a tactic definition *)
 
 and 'a gen_tactic_arg =
-  | TacDynamic     of Loc.t * Dyn.t
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 766222156..97917d2c7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1263,9 +1263,6 @@ module Make
           else str"(" ++ strm ++ str")"
 
         and pr_tacarg = function
-          | TacDynamic (loc,t) ->
-            pr_with_comments loc
-              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
             pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 29f679e71..b5a363371 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -672,7 +672,7 @@ and intern_tactic_seq onlytac ist = function
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
   | TacCall _ | Reference _
-  | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
+  | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
   | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
@@ -709,11 +709,6 @@ and intern_tacarg strict onlytac ist = function
   | TacGeneric arg ->
     let (_, arg) = Genintern.generic_intern ist arg in
     TacGeneric arg
-  | TacDynamic(loc,t) as x ->
-    if Dyn.has_tag t "value" then x
-    else
-      let tag = Dyn.tag t in
-      anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">")
 
 (* Reads the rules of a Match Context or a Match *)
 and intern_match_rule onlytac ist = function
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bb54a9cb7..850580f75 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -86,7 +86,7 @@ type tacvalue =
       Id.t option list * glob_tactic_expr
   | VRec of value Id.Map.t ref * glob_tactic_expr
 
-let (wit_tacvalue : (Empty.t, Empty.t, tacvalue) Genarg.genarg_type) =
+let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
   Genarg.create_arg None "tacvalue"
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
@@ -210,13 +210,6 @@ let pr_inspect env expr result =
 let constr_of_id env id =
   Term.mkVar (let _ = Environ.lookup_named id env in id)
 
-(* To embed tactics *)
-
-let ((value_in : value -> Dyn.t),
-     (value_out : Dyn.t -> value)) = Dyn.create "value"
-
-let valueIn t = TacDynamic (Loc.ghost, value_in t)
-
 (** Generic arguments : table of interpretation functions *)
 
 let push_trace call ist = match TacStore.get ist.extra f_trace with
@@ -1453,13 +1446,6 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
         Proofview.tclUNIT (Value.of_int i)
       end
   | Tacexp t -> val_interp ist t
-  | TacDynamic(_,t) ->
-      let tg = (Dyn.tag t) in
-      if String.equal tg "value" then
-        Ftactic.return (value_out t)
-      else
-        Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
-	  (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")
 
 (* Interprets an application node *)
 and interp_app loc ist fv largs : typed_generic_argument Ftactic.t =
@@ -2356,7 +2342,7 @@ let () =
 let () =
   let interp ist gl tac =
     let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
-    (project gl, TacArg (dloc, valueIn (of_tacvalue f)))
+    (project gl, TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f)))
   in
   Geninterp.register_interp0 wit_tactic interp
 
@@ -2365,6 +2351,9 @@ let () =
      project gl , interp_uconstr ist (pf_env gl) c
   )
 
+let () =
+  Geninterp.register_interp0 wit_tacvalue (fun ist gl c -> project gl, c)
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c7364ee62..88802bf35 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -45,9 +45,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env ->
 (** Given an interpretation signature, extract all values which are coercible to
     a [constr]. *)
 
-(** To embed several objects in Coqast.t *)
-val valueIn : value -> raw_tactic_arg
-
 (** Sets the debugger mode *)
 val set_debug : debug_info -> unit
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index fd7eaafbc..f5b6c3250 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -266,11 +266,6 @@ and subst_tacarg subst = function
   | TacNumgoals -> TacNumgoals
   | Tacexp t -> Tacexp (subst_tactic subst t)
   | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
-  | TacDynamic(the_loc,t) as x ->
-      (match Dyn.tag t with
-	| "value" -> x
-	| s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
-                 (str "Unknown dynamic: <" ++ str s ++ str ">"))
 
 (* Reads the rules of a Match Context or a Match *)
 and subst_match_rule subst = function