From 97da8221e0097ed365f0a99e4960148424a59734 Mon Sep 17 00:00:00 2001 From: glondu Date: Fri, 28 Oct 2011 08:35:06 +0000 Subject: 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 --- pretyping/glob_term.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'pretyping/glob_term.ml') 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 *) -- cgit v1.2.3