Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.

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)