diff options
Diffstat (limited to 'contrib/funind/rawtermops.ml')
| -rw-r--r-- | contrib/funind/rawtermops.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index 92396af590..ffd7cd007d 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -176,6 +176,7 @@ let change_vars = change_vars mapping lhs, change_vars mapping rhs ) + | RRecord _ -> error "Records are not supported" | RRec _ -> error "Local (co)fixes are not supported" | RSort _ -> rt | RHole _ -> rt @@ -358,6 +359,7 @@ let rec alpha_rt excluded rt = alpha_rt excluded rhs ) | RRec _ -> error "Not handled RRec" + | RRecord _ -> error "Not handled RRecord" | RSort _ -> rt | RHole _ -> rt | RCast (loc,b,CastConv (k,t)) -> @@ -409,6 +411,7 @@ let is_free_in id = | RIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 + | RRecord _ -> raise (UserError ("", str "Not handled RRecord")) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> false | RHole _ -> false @@ -507,6 +510,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | RRec _ -> raise (UserError("",str "Not handled RRec")) + | RRecord _ -> raise (UserError("",str "Not handled RRecord")) | RSort _ -> rt | RHole _ -> rt | RCast(loc,b,CastConv(k,t)) -> @@ -604,6 +608,8 @@ let ids_of_rawterm c = | RCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) | RRec _ -> failwith "Fix inside a constructor branch" + | RRecord (loc,w,l) -> Option.cata (ids_of_rawterm []) [] w @ + List.flatten (List.map (fun ((_,id), x) -> id :: ids_of_rawterm [] x) l) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] in (* build the set *) @@ -661,6 +667,7 @@ let zeta_normalize = zeta_normalize_term lhs, zeta_normalize_term rhs ) + | RRecord _ -> raise (UserError("",str "Not handled RRecord")) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt @@ -705,6 +712,7 @@ let expand_as = | RIf(loc,e,(na,po),br1,br2) -> RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) + | RRecord _ -> error "Not handled RRecord" | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) |