From c6f24b1cbfb485dbf14b3934208c113140de2eca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 5 Apr 2017 13:07:19 +0200
Subject: Fixing #5454 (an assert false with 'pat).

Note: Apparently not easy to make a test file as the error is raised
in "G_vernac.fresh_var" at parsing time (not captured by Fail).
---
 interp/topconstr.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a397ca82eb..bf0ce60d88 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -58,7 +58,9 @@ 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
+  | CPatCast (loc,_,_) ->
+     CErrors.user_err_loc (loc, "cases_pattern_fold_names",
+                           Pp.strbrk "Casts are not supported here.")
 
 let ids_of_pattern =
   cases_pattern_fold_names Id.Set.add Id.Set.empty
-- 
cgit v1.2.3