diff options
Diffstat (limited to 'pretyping/rawterm.ml')
| -rw-r--r-- | pretyping/rawterm.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index d7e3ac77..aaf9e63d 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 9535 2007-01-26 09:26:08Z jforest $ *) +(* $Id: rawterm.ml 9976 2007-07-12 11:58:30Z msozeau $ *) (*i*) open Util @@ -47,8 +47,8 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type cast_type = - | CastConv of cast_kind +type 'a cast_type = + | CastConv of cast_kind * 'a | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) type rawconstr = @@ -68,7 +68,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * cast_type * rawconstr + | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr @@ -120,7 +120,7 @@ let map_rawconstr f = function | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) - | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t) + | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -190,7 +190,7 @@ let occur_rawconstr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | RCast (loc,c,_,t) -> (occur c) or (occur t) + | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -247,7 +247,8 @@ let free_rawvars = vars bounded1 vs2 bv.(i) in array_fold_left_i vars_fix vs idl - | RCast (loc,c,_,t) -> vars bounded (vars bounded vs c) t + | RCast (loc,c,k) -> let v = vars bounded vs c in + (match k with CastConv (_,t) -> vars bounded v t | _ -> v) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = @@ -280,7 +281,7 @@ let loc_of_rawconstr = function | RRec (loc,_,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc - | RCast (loc,_,_,_) -> loc + | RCast (loc,_,_) -> loc | RDynamic (loc,_) -> loc (**********************************************************************) |