From 6f89e06a3230c3932cb43bd28e0f07f47d954a3f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Apr 2010 12:05:15 +0000
Subject: Fixed some printing bugs. - Notations with coercions to funclass
 inserted were not working any   longer since r11886. Made a fix but maybe
 should we eventually type   the notations so that they have a canonical form
 (and in particular   with coercions pre-inserted?). - Improved spacing
 management in printing extra tactic arguments "by" and "in".

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 24f5a78c5e..99c627a956 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -592,6 +592,10 @@ let rec remove_coercions inctx = function
       with Not_found -> c)
   | c -> c
 
+let rec flatten_application = function
+  | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l))
+  | a -> a
+
 let rec rename_rawconstr_var id0 id1 = function
     RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1)
   | RVar(loc,id) when id=id0 -> RVar(loc,id1)
@@ -632,8 +636,9 @@ let rec extern inctx scopes vars r =
     extern_optimal_prim_token scopes r r'
   with No_match ->
   try
+    let r'' = flatten_application r' in
     if !Flags.raw_print or !print_no_symbol then raise No_match;
-    extern_symbol scopes vars r' (uninterp_notations r')
+    extern_symbol scopes vars r'' (uninterp_notations r'')
   with No_match -> match r' with
   | RRef (loc,ref) ->
       extern_global loc (implicits_of_global ref)
-- 
cgit v1.2.3