From 50a39015ea0c86cdb6d368ff7f92ce2091085146 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:19:27 +0100
Subject: Fixing a notation printing bug (missing a @ to reflect absence of
 imp. args).

When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
---
 interp/constrextern.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82ba559406..5098b2a00c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1216,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
               (* 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
-          | None when nallargs > 0 ->
+          | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
@@ -1226,7 +1226,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
             | _ -> t, [], [], []
             end
-          | None -> t, [], [], []
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
-- 
cgit v1.2.3