diff options
Diffstat (limited to 'contrib/funind/indfun.ml')
| -rw-r--r-- | contrib/funind/indfun.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 320bac830..b6b2cbd11 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) -> |