From 0f434208acc9e16382839f343b45d24aeaba0afd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Apr 2020 21:31:27 +0200
Subject: Removing a useless explicit use of subscopes in interpreting
 arguments of a notation.

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

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d4090117b0..c7c298cd5b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1822,8 +1822,8 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
       DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
     | NApp (NRef g,pl) ->
       ensure_kind test_kind ?loc g;
-      let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      let pl = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in
+      let (_,argscs2) = find_remaining_scopes pl args g in
+      let pl = List.map (in_not test_kind_inner loc scopes fullsubst []) pl in
       let pl = add_local_defs_and_check_length loc genv g pl args in
       let args = List.map2 (fun x -> in_pat test_kind_inner (x,snd scopes)) argscs2 args in
       let pat =
-- 
cgit v1.2.3