From 081a649157d2460c924404cd51b4ba50c23b1956 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 21 Aug 2015 19:45:39 +0200
Subject: Fixing #4318 (anomaly when applying args to a recursive notation in
 patterns).

I don't know what was the intent of Pierre B here. In 8.4, it was not
supported, raising with an error at parsing time. I changed the
anomaly into an error at interpretation time, so it is still not
supported but we could support it if some legitimate use of it
eventually appears.
---
 interp/constrintern.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8c56d0ccfe..ecaf2b8c13 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1214,7 +1214,8 @@ let drop_notations_pattern looked_for =
 		 List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl,
 		 List.map2 (in_pat_sc env) argscs2 args)
     | NList (x,_,iter,terminator,lassoc) ->
-      let () = assert (List.is_empty args) in
+      if not (List.is_empty args) then user_err_loc
+        (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
          (* All elements of the list are in scopes (scopt,subscopes) *)
 	 let (l,(scopt,subscopes)) = Id.Map.find x substlist in
-- 
cgit v1.2.3