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 --- pretyping/pretyping.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3