From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 parsing/ppvernac.ml | 40 ++++++++++++++++++++++++++--------------
 1 file changed, 26 insertions(+), 14 deletions(-)

(limited to 'parsing/ppvernac.ml')

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0b6e5771..aea44604 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 8624 2006-03-13 17:38:17Z msozeau $ *)  
+(* $Id: ppvernac.ml 8831 2006-05-19 09:29:54Z herbelin $ *)  
 
 open Pp
 open Names
@@ -277,7 +277,7 @@ let pr_onescheme (id,dep,ind,s) =
   hov 0 (pr_lident id ++ str" :=") ++ spc() ++
   hov 0 ((if dep then str"Induction for" else str"Minimality for")
   ++ spc() ++ pr_reference ind) ++ spc() ++ 
-  hov 0 (str"Sort" ++ spc() ++ pr_sort s)
+  hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
 
 let begin_of_inductive = function
     [] -> 0
@@ -555,18 +555,23 @@ let rec pr_vernac = function
               else ([],def,type_) in
             let bl = bl @ bl' in
             let ids = List.flatten (List.map name_of_binder bl) in
-            let name =
-              try snd (List.nth ids n)
-              with Failure _ ->
-                warn (str "non-printable fixpoint \""++pr_id id++str"\"");
-                Anonymous in
             let annot =
-	      match (ro : Topconstr.recursion_order_expr) with
-		  CStructRec -> 
-		    if List.length ids > 1 then 
-                      spc() ++ str "{struct " ++ pr_name name ++ str"}"
-		    else mt()
-		| CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}"
+	      match n with 
+		| None -> mt () 
+		| Some n -> 
+		    let name =
+		      try snd (List.nth ids n)
+		      with Failure _ ->
+			warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+			Anonymous in
+		    match (ro : Topconstr.recursion_order_expr) with
+			CStructRec -> 
+			  if List.length ids > 1 then 
+			    spc() ++ str "{struct " ++ pr_name name ++ str"}"
+			  else mt()
+		      | CWfRec c -> 
+			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
+			    pr_lconstr_expr c ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -823,6 +828,13 @@ and pr_extend s cl =
   try
     let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
     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 ->
+	    (* Will put an unnecessary extra space in front *)
+	    pr_gen (Global.env()) (List.hd cl), rl, List.tl cl 
+	| [] -> anomaly "Empty entry" in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
@@ -831,7 +843,7 @@ and pr_extend s cl =
                 (strm ++ pr_gen (Global.env()) (List.hd args),
                 List.tl args)
             | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
-        (mt(),cl) rl in
+        (start,cl) rl in
     hov 1 pp
   with Not_found ->
     hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
-- 
cgit v1.2.3