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

1 files changed, 6 insertions, 1 deletions

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)