aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-28 16:48:34 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-28 16:48:34 +0000
commit7c151ae076fe5ebba9a2ea507f8f4a235feab9c7 (patch)
tree2728b48d7d7cbe0bac436de51394ec23c6f52fbb /plugins
parentd96ec0f0a094ce84890297be342bc129d0d6b47b (diff)
Make usage of Dyn explicit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r--plugins/subtac/subtac.ml1
-rw-r--r--plugins/subtac/subtac_command.ml1
-rw-r--r--plugins/subtac/subtac_pretyping.ml1
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml3
4 files changed, 1 insertions, 5 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 56134d708..97a929809 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 d1e890867..937f7d065 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 e705e73c1..845710540 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 f818379e7..3e275cd0f 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