From a905e70df85ef7bf700bb3d6a1b48ae180dfa987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 13:42:35 +0100
Subject: Inherit arguments scopes in pattern notations bound to some @id.

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

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1b9b45c3fb..f68f4e67b9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,10 +1659,11 @@ let drop_notations_pattern looked_for genv =
           let () = assert (List.is_empty vars) in
           let (_,argscs) = find_remaining_scopes [] pats g in
           Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
-        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
+        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
               test_kind top g;
               let () = assert (List.is_empty vars) in
-              Some (g, List.map (in_pat false scopes) pats, [])
+              let (_,argscs) = find_remaining_scopes [] pats g in
+              Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
         | NApp (NRef g,args) ->
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
               test_kind top g;
-- 
cgit v1.2.3