From 7c151ae076fe5ebba9a2ea507f8f4a235feab9c7 Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 28 Oct 2009 16:48:34 +0000
Subject: Make usage of Dyn explicit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac.ml             | 1 -
 plugins/subtac/subtac_command.ml     | 1 -
 plugins/subtac/subtac_pretyping.ml   | 1 -
 plugins/subtac/subtac_pretyping_F.ml | 3 +--
 4 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3