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

4 files changed, 20 insertions, 4 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)
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index e6eefea8ab..adf8275ee8 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -184,7 +184,7 @@ ARGUMENT EXTEND hloc
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
@@ -200,8 +200,8 @@ let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds =
     | None,true -> str "in" ++ spc () ++ str "*"
     | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
     | Some l,_ ->
-	str "in" ++ spc () ++
-	  Util.prlist_with_sep spc pr_id l ++
+	str "in" ++
+	  Util.prlist (fun id -> spc () ++ pr_id id) l ++
 	  match concl with
 	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
 	    | _ -> mt ()
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index aca872970c..c1a7e961a9 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -1,4 +1,6 @@
 2 3
      : PAIR
+2[+]3
+     : nat
 forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
      : Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 0d5cc9e24c..3eeff401cf 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -6,6 +6,15 @@ Inductive PAIR := P (n1:nat) (n2:nat).
 Coercion P : nat >-> Funclass.
 Check (2 3).
 
+(* Check that notations with coercions to functions inserted still work *)
+(* (were not working from revision 11886 to 12951) *)
+
+Record Binop := { binop :> nat -> nat -> nat }.
+Class Plusop := { plusop : Binop; z : nat }.
+Infix "[+]" := plusop (at level 40).
+Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}.
+Check 2[+]3.
+
 (* Test bug #2091 (variable le was printed using <= !) *)
 
 Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.