From 67e16fdeef26455d0afa357e31de8f7b3f772034 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:30:05 +0100
Subject: Fixing printing of notations bound to an expression of the form "@f".

The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.

It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
---
 interp/constrextern.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5098b2a00c..681d6ba541 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1209,23 +1209,17 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             [], [] in
         (* Adjust to the number of arguments expected by the notation *)
         let (t,args,argsscopes,argsimpls) = match n with
-          | Some n when nallargs >= n && nallargs > 0 ->
+          | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
               let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
               (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
-              (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
-              args2, args2scopes, args2impls
+              DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | Some 0 when nallargs = 0 ->
-            begin match DAst.get f with
-            | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
-            | _ -> t, [], [], []
-            end
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
-- 
cgit v1.2.3