diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 763261bfd..32d9f107c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -942,6 +942,8 @@ let rec raw_of_pat env = function | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) -> let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) + | PCase (_,PMeta None,tm,[||]) -> + RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[]) | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> let brs = Array.to_list (Array.map (raw_of_pat env) bv) in let brns = Array.to_list cstr_nargs in |