Pretty printing of generalized binder

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

1 files changed, 19 insertions, 13 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index d6c3cbb9c..fa0755364 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -219,27 +219,33 @@ let surround_impl k p =
   | Explicit -> str"(" ++ p ++ str")"
   | Implicit -> str"{" ++ p ++ str"}"
 
-let surround_binder k p =
-  match k with
-  | Default b -> hov 1 (surround_impl b p)
-  | Generalized (b, b', t) ->
-      hov 1 (str"`" ++ (surround_impl b' p))
-
 let surround_implicit k p =
   match k with
-  | Default Explicit -> p
-  | Default Implicit -> (str"{" ++ p ++ str"}")
-  | Generalized (b, b', t) ->
-      str"`" ++ (surround_impl b' p)
+  | Explicit -> p
+  | Implicit -> (str"{" ++ p ++ str"}")
 
 let pr_binder many pr (nal,k,t) =
+  match k with
+    | Generalized (b, b', t') ->
+      assert (b=Implicit);
+      begin match nal with
+	|[loc,Anonymous] ->
+	  hov 1 (str"`" ++ (surround_impl b'
+			      ((if t' then str "!" else mt ()) ++ pr t)))
+	|[loc,Name id] ->
+	  hov 1 (str "`" ++ (surround_impl b'
+			       (pr_lident (loc,id) ++ str " : " ++
+				  (if t' then str "!" else mt()) ++ pr t)))
+	|_ -> anomaly "List of generalized binders have alwais one element."
+      end
+    | Default b ->
       match t with
 	| CHole _ ->
 	  let s = prlist_with_sep spc pr_lname nal in
-	  hov 1 (surround_implicit k s)
+	  hov 1 (surround_implicit b s)
 	| _ ->
-	  let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
-	  hov 1 (if many then surround_binder k s else surround_implicit k s)
+	  let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in
+	  hov 1 (if many then surround_impl b s else surround_implicit b s)
 
 let pr_binder_among_many pr_c = function
   | LocalRawAssum (nal,k,t) ->