diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/indfun.ml | 1 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 4 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 8 |
3 files changed, 1 insertions, 12 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 320bac8302..b6b2cbd11d 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -212,7 +212,6 @@ let rec is_rec names = | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false | RCast(_,b,_) -> lookup names b | RRec _ -> error "RRec not handled" - | RRecord _ -> error "Not handled RRecord" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 48a96f8b6c..c16e645c73 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -583,7 +583,6 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = *) build_entry_lc env funnames avoid (mkRApp(b,args)) | RRec _ -> error "Not handled RRec" - | RRecord _ -> error "Not handled RRecord" | RProd _ -> error "Cannot apply a type" end (* end of the application treatement *) @@ -686,7 +685,6 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = end | RRec _ -> error "Not handled RRec" - | RRecord _ -> error "Not handled RRecord" | RCast(_,b,_) -> build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" @@ -1026,7 +1024,7 @@ let rec compute_cst_params relnames params = function discriminitation ones *) | RSort _ -> params | RHole _ -> params - | RIf _ | RRecord _ | RRec _ | RCast _ | RDynamic _ -> + | RIf _ | RRec _ | RCast _ | RDynamic _ -> raise (UserError("compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index ffd7cd007d..92396af590 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -176,7 +176,6 @@ 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 @@ -359,7 +358,6 @@ 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)) -> @@ -411,7 +409,6 @@ 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 @@ -510,7 +507,6 @@ 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)) -> @@ -608,8 +604,6 @@ 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 *) @@ -667,7 +661,6 @@ 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 @@ -712,7 +705,6 @@ 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)) |