From 0e96c241550c4a8abf65f3bb63fcd7cab3380e92 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 7 Aug 2020 20:54:55 -0700
Subject: Document semantic restriction on patterns

---
 interp/constrintern.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6d4ab8b4d6..1d3b1bbb24 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1724,8 +1724,7 @@ let drop_notations_pattern looked_for genv =
          the domains of lambdas in the encoding of match in constr.
          This check is here and not in the parser because it would require
          duplicating the levels of the [pattern] rule. *)
-      CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
-                            (Pp.strbrk "Casts are not supported in this pattern.")
+      CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.")
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
   and in_not top loc scopes (subst,substlist as fullsubst) args = function
     | NVar id ->
-- 
cgit v1.2.3