diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 16:48:34 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 16:48:34 +0000 |
| commit | 7c151ae076fe5ebba9a2ea507f8f4a235feab9c7 (patch) | |
| tree | 2728b48d7d7cbe0bac436de51394ec23c6f52fbb /pretyping | |
| parent | d96ec0f0a094ce84890297be342bc129d0d6b47b (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 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 956b778e0..eaa2e6757 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 |