diff options
Diffstat (limited to 'contrib/funind/rawterm_to_relation.ml')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 48a96f8b6..c16e645c7 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 |