Fix printing of instances, generalized arguments.

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

2 files changed, 9 insertions, 20 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4970ca131..934850072 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -223,14 +223,14 @@ let surround_binder k p =
   match k with
   | Default b -> hov 1 (surround_impl b p)
   | Generalized (b, b', t) ->
-      hov 1 (surround_impl b' (surround_impl b p))
+      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) ->
-      surround_impl b' (surround_impl b p)
+      str"`" ++ (surround_impl b' p)
 
 let pr_binder many pr (nal,k,t) =
   match t with
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c858439e6..1fa57878d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -690,34 +690,23 @@ let rec pr_vernac = function
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)
 
-
-(*   | VernacClass (id, par, ar, sup, props) -> *)
-(*       hov 1 ( *)
-(* 	str"Class" ++ spc () ++ pr_lident id ++ *)
-(* (\* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *\) *)
-(* 	  pr_and_type_binders_arg par ++ *)
-(* 	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_glob_sort (snd ar) | None -> mt()) ++ *)
-(* 	  spc () ++ str":=" ++ spc () ++ *)
-(* 	  prlist_with_sep (fun () -> str";" ++ spc())  *)
-(* 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *)
-
  | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
        pr_non_locality (not glob) ++
        (if abst then str"Declare " else mt ()) ++
-       str"Instance" ++ spc () ++
-	 pr_and_type_binders_arg sup ++
-	 str"=>" ++ spc () ++
-	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
-	 pr_constr_expr cl ++ spc () ++
+       str"Instance" ++ 
+       (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | 
+	Anonymous -> mt ()) ++
+       pr_and_type_binders_arg sup ++
+       str":" ++ spc () ++	 
+       pr_constr_expr cl ++ spc () ++
 	 (match props with
 	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p
 	  | None -> mt()))
 
  | VernacContext l ->
      hov 1 (
-       str"Context" ++ spc () ++ str"[" ++ spc () ++
-	 pr_and_type_binders_arg l ++ spc () ++ str "]")
+       str"Context" ++ spc () ++ pr_and_type_binders_arg l)
 
 
  | VernacDeclareInstances (glob, ids) ->