Fixing multiple printing bugs with "Notation f x := ..."

- Missing space and bad constr level in "About f"
- Display of arguments missing when used as a pattern notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 38 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 08db24dbaa..de97257ff4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -272,6 +272,10 @@ let make_pat_notation loc ntn (terms,termlists as subst) =
     (fun (loc,p) -> CPatPrim (loc,p))
     destPatPrim terms
 
+let mkPat loc qid l =
+  (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
+  if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
+
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try
@@ -326,15 +330,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	(match keyrule with
         | NotationRule (sc,ntn) -> raise No_match
         | SynDefRule kn ->
-	    let p =
-	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
-	      if l = [] then
-		CPatAtom (loc,Some qid)
-	      else
-		let l =
-		  List.map (extern_cases_pattern_in_scope allscopes vars) l in
-		CPatCstr (loc,qid,l) in
-	    insert_pat_alias loc p na)
+	    let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+	    let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in
+	    insert_pat_alias loc (mkPat loc qid l) na)
       | PatCstr (_,f,l,_), Some n when List.length l > n ->
 	  raise No_match
       | PatCstr (loc,_,_,na),_ ->
@@ -361,8 +359,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 		  insert_pat_delimiters loc
 		    (make_pat_notation loc ntn (l,ll)) key)
           | SynDefRule kn ->
-	      let qid = shortest_qualid_of_syndef vars kn in
-              CPatAtom (loc,Some (Qualid (loc, qid))) in
+	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+	      let l =
+		List.map (fun (c,(scopt,scl)) ->
+                  extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) 
+                  subst in
+              assert (substlist = []);
+	      mkPat loc qid l in
 	insert_pat_alias loc p na
       | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
       | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 17feae4ed1..87f11030ef 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -458,13 +458,15 @@ let gallina_print_constant_with_infos sp =
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def kn =
-  let sep = " := "
-  and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
+  let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
   let c = Topconstr.glob_constr_of_aconstr dummy_loc a in
-  str "Notation " ++ pr_qualid qid ++
-  prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
-  Constrextern.without_symbols pr_lglob_constr c ++ fnl ()
+  hov 2
+    (hov 4
+       (str "Notation " ++ pr_qualid qid ++
+        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ 
+        spc () ++ str ":=") ++
+     spc () ++ Constrextern.without_symbols pr_glob_constr c) ++ fnl ()
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 444d6b0910..5a4a72303c 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -27,3 +27,13 @@ let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
+Notation plus2 n := (S (S n))
+λ n : list(nat),
+match n with
+| nil => 2
+| 0 :: _ => 2
+| list1 => 0
+| 1 :: _ :: _ => 2
+| plus2 _ :: _ => 2
+end
+     : list(nat) -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e7b0b97546..635b254166 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -60,6 +60,13 @@ Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
 Check fun f x => f x + S x.
 
+Open Scope list_scope.
+Notation list1 := (1::nil)%list.
+Notation plus2 n := (S (S n)).
+(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
+Print plus2.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder