- Cleaning (unification of ML names, removal of obsolete code,

  reorganization of code) and documentation (in pcoq.mli) of the code
  for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
  Notation, Notation); merged the two copies of interp_entry_name to
  avoid they diverge.  
- Added support in Tactic Notation for ne_..._list_sep in general and
  for (ne_)ident_list(_sep) in particular.



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

1 files changed, 11 insertions, 9 deletions

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0054326e40..be04f584d9 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -73,7 +73,7 @@ let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac
 
 let rec extract_signature = function
   | [] -> []
-  | Egrammar.TacNonTerm (_,(_,t),_) :: l -> t :: extract_signature l
+  | Egrammar.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
   | _::l -> extract_signature l
 
 let rec match_vernac_rule tys = function
@@ -119,9 +119,11 @@ let strip_meta id =
   else id
 
 let pr_production_item = function
-  | VNonTerm (loc,nt,Some p) -> str nt ++ str"(" ++ pr_id (strip_meta p) ++ str")"
-  | VNonTerm (loc,nt,None) -> str nt
-  | VTerm s -> qs s
+  | TacNonTerm (loc,nt,Some (p,sep)) ->
+      let pp_sep = if sep <> "" then str "," ++ quote (str sep) else mt () in
+      str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
+  | TacNonTerm (loc,nt,None) -> str nt
+  | TacTerm s -> qs s
 
 let pr_comment pr_c = function
   | CommentConstr c -> pr_c c
@@ -811,7 +813,7 @@ let rec pr_vernac = function
 	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
 	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env 
-	  (idl @ List.map coerce_global_to_id 
+	  (idl @ List.map coerce_reference_to_id 
 	    (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
 	  (Global.env())
 	  body in
@@ -945,15 +947,15 @@ and pr_extend s cl =
     let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
     let start,rl,cl =
       match rl with
-      | Egrammar.TacTerm s :: rl -> str s, rl, cl
-      | Egrammar.TacNonTerm _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl 
+      | Egrammar.GramTerminal s :: rl -> str s, rl, cl
+      | Egrammar.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl 
       | [] -> anomaly "Empty entry" in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
           let pp,args = match pi with
-          | Egrammar.TacNonTerm _ -> (pr_arg (List.hd args), List.tl args)
-          | Egrammar.TacTerm s -> (str s, args) in
+          | Egrammar.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
+          | Egrammar.GramTerminal s -> (str s, args) in
           (strm ++ spc() ++ pp), args)
         (start,cl) rl in
     hov 1 pp