diff options
author | 2011-10-28 08:35:06 +0000 | |
---|---|---|
committer | 2011-10-28 08:35:06 +0000 | |
commit | 97da8221e0097ed365f0a99e4960148424a59734 (patch) | |
tree | 7a0d1b1bc8995dd456b38863674a65230ace957f /pretyping | |
parent | 7a10a8a17928df1da29b4f69a2b54ac83a3e1fc3 (diff) |
Remove dynamic stuff from constr_expr and glob_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/detyping.ml | 1 | ||||
-rw-r--r-- | pretyping/glob_term.ml | 11 | ||||
-rw-r--r-- | pretyping/glob_term.mli | 1 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 9 |
4 files changed, 4 insertions, 18 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index fd85d15f7..bb1ced154 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -669,7 +669,6 @@ let rec subst_glob_constr subst raw = | CastCoerce -> let r1' = subst_glob_constr subst r1 in if r1' == r1 then raw else GCast (loc,r1',k)) - | GDynamic _ -> raw (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 85dcf291c..a4113671f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -67,7 +67,6 @@ type glob_constr = | GSort of loc * glob_sort | GHole of (loc * hole_kind) | GCast of loc * glob_constr * glob_constr cast_type - | GDynamic of loc * Dyn.t and glob_decl = name * binding_kind * glob_constr option * glob_constr @@ -144,7 +143,7 @@ let map_glob_constr_left_to_right f = function let comp1 = f c in let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in GCast (loc,comp1,comp2) - | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) as x -> x + | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x let map_glob_constr = map_glob_constr_left_to_right @@ -183,7 +182,6 @@ let map_glob_constr_with_binders_loc loc g f e = function | GRef (_,x) -> GRef (loc,x) | GEvar (_,x,l) -> GEvar (loc,x,l) | GPatVar (_,x) -> GPatVar (loc,x) - | GDynamic (_,x) -> GDynamic (loc,x) *) let fold_glob_constr f acc = @@ -206,7 +204,7 @@ let fold_glob_constr f acc = fold (Option.fold_left fold acc bbd) bty)) acc bl in Array.fold_left fold (Array.fold_left fold acc tyl) bv | GCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> acc + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc and fold_pattern acc (_,idl,p,c) = fold acc c @@ -245,7 +243,7 @@ let occur_glob_constr id = occur_fix bl) idl bl tyl bv) | GCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> false + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -303,7 +301,7 @@ let free_glob_vars = array_fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bounded vs c in (match k with CastConv (_,t) -> vars bounded v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> vs + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = let bounded' = List.fold_right Idset.add idl bounded in @@ -336,7 +334,6 @@ let loc_of_glob_constr = function | GSort (loc,_) -> loc | GHole (loc,_) -> loc | GCast (loc,_,_) -> loc - | GDynamic (loc,_) -> loc (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index c445bcd24..7fb995a88 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -71,7 +71,6 @@ type glob_constr = | GSort of loc * glob_sort | GHole of (loc * Evd.hole_kind) | GCast of loc * glob_constr * glob_constr cast_type - | GDynamic of loc * Dyn.t and glob_decl = name * binding_kind * glob_constr option * glob_constr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 978feec7c..901936f33 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -679,15 +679,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon - | GDynamic (loc,d) -> - if (Dyn.tag d) = "constr" then - let c = constr_out d in - let j = (Retyping.get_judgment_of env !evdref c) in - j - (*inh_conv_coerce_to_tycon loc env evdref j tycon*) - else - user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic.")) - (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type valcon env evdref lvar = function | GHole loc -> |