From 232b8230833440b5bd982d6d434e8ca111a62d49 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Jul 2018 11:37:08 +0200
Subject: Fixes #8126 (issue with notations and nested applications).

No reason not to collapse inner applications with explicit arguments.
This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
---
 interp/constrintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cb50245d5a..f5022d485b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1891,9 +1891,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
 	    lvar us args ref 
 	in
-	  (* Rem: GApp(_,f,[]) stands for @f *)
-	DAst.make ?loc @@
-	  GApp (f, intern_args env args_scopes (List.map fst args))
+        (* Rem: GApp(_,f,[]) stands for @f *)
+        if args = [] then DAst.make ?loc @@ GApp (f,[]) else
+          smart_gapp f loc (intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
         let f,args = match f.CAst.v with
-- 
cgit v1.2.3