diff options
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r-- | interp/topconstr.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 91099bbb1..4109bdb7f 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -59,6 +59,7 @@ let rec cases_pattern_fold_names f a = function | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a + | CPatCast _ -> assert false let ids_of_pattern_list = List.fold_left @@ -92,6 +93,8 @@ let rec fold_local_binders g f n acc b = function f n (fold_local_binders g f n' acc b l) t | LocalRawDef ((_,na),t)::l -> f n (fold_local_binders g f (name_fold g na n) acc b l) t + | LocalPattern _::l -> + assert false | [] -> f n acc b @@ -170,6 +173,7 @@ let split_at_annot bl na = (List.rev ans, LocalRawAssum (r, k, t) :: rest) end | LocalRawDef _ as x :: rest -> aux (x :: acc) rest + | LocalPattern _ :: rest -> assert false | [] -> user_err_loc(loc,"", str "No parameter named " ++ Nameops.pr_id id ++ str".") @@ -191,7 +195,9 @@ let map_local_binders f g e bl = LocalRawAssum(nal,k,ty) -> (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) | LocalRawDef((loc,na),ty) -> - (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in + (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) + | LocalPattern _ -> + assert false in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) |