4 files changed, 1 insertions, 5 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