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

1 files changed, 14 insertions, 11 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)))