From 14196d8ab425f67faf3995bd29a003de3b2e87ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:26:14 +0100
Subject: Propagate implicit arguments in all notations for partial
 applications.

This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1cfd50e26e..e14629df9b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2070,9 +2070,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             | CRef (ref,us) ->
                intern_applied_reference ~isproj intern env
                  (Environ.named_context_val globalenv) lvar us args ref
-            | CNotation (_,ntn,([],[],[],[])) ->
+            | CNotation (_,ntn,ntnargs) ->
                 assert (Option.is_empty isproj);
-                let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
+                let c = intern_notation intern env ntnvars loc ntn ntnargs in
                 let x, impl, scopes, l = find_appl_head_data c in
                   (x,impl,scopes,l), args
             | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
-- 
cgit v1.2.3