diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
| commit | ff1dde8f1585c92dd69a9a41ad709f15ef8936da (patch) | |
| tree | e7e87fb5d549e0bf19785e54737a96ee4d9917d6 /interp/constrextern.ml | |
| parent | a788b511487e6b748d5be35140a7ad2ca110936e (diff) | |
| parent | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff) | |
Merge commit 'upstream/8.1.pl2+dfsg'
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 349e8629..b9d7694f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: constrextern.ml 10135 2007-09-21 14:28:12Z herbelin $ *) (*i*) open Pp @@ -923,6 +923,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 |