From 08090c64a3322ca17e6af733831b66d9ffd0756c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 May 2003 01:20:19 +0000
Subject: Hack pour ameliorer l'affichage des applications dans les `...` et
 ``...`` en les mettant sous forme n-aire, et sans casser la compatibilite des
 implicites

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4018 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1032b0116d..13864febcb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -454,7 +454,12 @@ let internalise isarity sigma env allow_soapp lvar c =
 	    | CRef ref -> intern_reference env lvar ref
 	    | _ -> (intern false env f, [], [])
         in
-	  RApp (loc, c, intern_impargs c env impargs args_scopes args)
+	let args = intern_impargs c env impargs args_scopes args in
+	(match c with 
+	  | RApp (loc', f', args') ->
+	      (* May happen with the ``...`` and `...` grammars *)
+	      RApp (join_loc loc' loc, f',args'@args)
+	  | _ -> RApp (loc, c, args))
     | CCases (loc, po, tms, eqns) ->
 	RCases (loc, option_app (intern true env) po,
 		List.map (intern false env) tms,
-- 
cgit v1.2.3