Make usage of Dyn explicit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 10 insertions, 17 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 56134d7086..97a9298092 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -29,7 +29,6 @@ open Pretype_errors
 open Rawterm
 open Evarconv
 open Pattern
-open Dyn
 open Vernacexpr
 
 open Subtac_coercion
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index d1e890867c..937f7d0650 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -2,7 +2,6 @@ open Closure
 open RedFlags
 open Declarations
 open Entries
-open Dyn
 open Libobject
 open Pattern
 open Matching
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index e705e73c16..8457105407 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -29,7 +29,6 @@ open Pretype_errors
 open Rawterm
 open Evarconv
 open Pattern
-open Dyn
 
 open Subtac_coercion
 open Subtac_utils
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index f818379e73..3e275cd0fd 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -30,7 +30,6 @@ open Pretype_errors
 open Rawterm
 open Evarconv
 open Pattern
-open Dyn
 open Pretyping
 
 (************************************************************************)
@@ -530,7 +529,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref cj tycon
 
     | RDynamic (loc,d) ->
-	if (tag d) = "constr" then
+	if (Dyn.tag d) = "constr" then
 	  let c = constr_out d in
 	  let j = (Retyping.get_judgment_of env ( !evdref) c) in
 	    j
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 956b778e06..eaa2e67576 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -29,7 +29,6 @@ open Pretype_errors
 open Rawterm
 open Evarconv
 open Pattern
-open Dyn
 
 type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * unsafe_judgment) list
@@ -73,7 +72,7 @@ let search_guard loc env possible_indexes fixdefs =
 
 (* To embed constr in rawconstr *)
 let ((constr_in : constr -> Dyn.t),
-     (constr_out : Dyn.t -> constr)) = create "constr"
+     (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
 (** Miscellaneous interpretation functions *)
 
@@ -622,7 +621,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
     | RDynamic (loc,d) ->
-	if (tag d) = "constr" then
+	if (Dyn.tag d) = "constr" then
 	  let c = constr_out d in
 	  let j = (Retyping.get_judgment_of env !evdref c) in
 	    j
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bd0e9c7b42..13add4151f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -13,7 +13,6 @@ open Closure
 open RedFlags
 open Declarations
 open Entries
-open Dyn
 open Libobject
 open Pattern
 open Matching
@@ -141,15 +140,15 @@ 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))) =
-  create "tactic"
+  Dyn.create "tactic"
 
 let ((value_in : value -> Dyn.t),
-     (value_out : Dyn.t -> value)) = create "value"
+     (value_out : Dyn.t -> value)) = Dyn.create "value"
 
 let valueIn t = TacDynamic (dummy_loc,value_in t)
 let valueOut = function
   | TacDynamic (_,d) ->
-    if (tag d) = "value" then
+    if (Dyn.tag d) = "value" then
       value_out d
     else
       anomalylabstrm "valueOut" (str "Dynamic tag should be value")
@@ -894,7 +893,7 @@ and intern_tacarg strict ist = function
   | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
   | Tacexp t -> Tacexp (intern_tactic ist t)
   | TacDynamic(loc,t) as x ->
-      (match tag t with
+      (match Dyn.tag t with
 	| "tactic" | "value" | "constr" -> x
 	| s -> anomaly_loc (loc, "",
                  str "Unknown dynamic: <" ++ str s ++ str ">"))
@@ -1864,7 +1863,7 @@ and interp_tacarg ist gl = function
       VIntroPattern (IntroIdentifier id)
   | Tacexp t -> val_interp ist gl t
   | TacDynamic(_,t) ->
-      let tg = (tag t) in
+      let tg = (Dyn.tag t) in
       if tg = "tactic" then
         val_interp ist gl (tactic_out t ist)
       else if tg = "value" then
@@ -2727,7 +2726,7 @@ and subst_tacarg subst = function
   | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
   | Tacexp t -> Tacexp (subst_tactic subst t)
   | TacDynamic(the_loc,t) as x ->
-      (match tag t with
+      (match Dyn.tag t with
 	| "tactic" | "value" -> x
         | "constr" ->
           TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
@@ -2941,7 +2940,7 @@ let tacticIn t =
 
 let tacticOut = function
   | TacArg (TacDynamic (_,d)) ->
-    if (tag d) = "tactic" then
+    if (Dyn.tag d) = "tactic" then
       tactic_out d
     else
       anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 238a329fd9..307e3a97dd 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -9,7 +9,6 @@
 (*i $Id$ i*)
 
 (*i*)
-open Dyn
 open Pp
 open Util
 open Names