From 456ced60ef1fc71f8f914e07b80831fa6dd46ea5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 13 Apr 2016 07:56:44 +0200
Subject: Fixing printing of Instance.

---
 printing/ppconstr.ml     | 12 ++++++++----
 printing/ppconstrsig.mli |  1 +
 printing/ppvernac.ml     |  5 ++++-
 3 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1866ca504..eead3a684 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -493,6 +493,11 @@ end) = struct
       pr (lapp,L) a  ++
         prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
+  let pr_record_body_gen pr l =
+    spc () ++
+    prlist_with_sep pr_semicolon
+      (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l
+
   let pr_forall () = keyword "forall" ++ spc ()
 
   let pr_fun () = keyword "fun" ++ spc ()
@@ -595,10 +600,7 @@ end) = struct
         return (pr_app (pr mt) a l, lapp)
       | CRecord (_,l) ->
         return (
-          hv 0 (str"{|" ++ spc () ++
-                  prlist_with_sep pr_semicolon
-                  (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
-                ++ str" |}"),
+          hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
           latom
         )
       | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
@@ -731,6 +733,8 @@ end) = struct
 
   let pr_cases_pattern_expr = pr_patt ltop
 
+  let pr_record_body = pr_record_body_gen pr
+
   let pr_binders = pr_undelimited_binders spc (pr ltop)
 
 end
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index c711dd8f7..a59fc6d67 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -50,6 +50,7 @@ module type Pp = sig
     ('a * Names.Id.t) option * recursion_order_expr ->
     std_ppcmds
 
+  val pr_record_body : (reference * constr_expr) list -> std_ppcmds
   val pr_binders : local_binder list -> std_ppcmds
   val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
   val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 1bd053d9d..b1464bf16 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -891,9 +891,12 @@ module Make
                  | (_, Anonymous), _ -> mt ()) ++
                 pr_and_type_binders_arg sup ++
                 str":" ++ spc () ++
+                (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
                 pr_constr cl ++ pr_priority pri ++
                 (match props with
-                  | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
+                  | Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+                  | Some (true,_) -> assert false
+                  | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
                   | None -> mt()))
           )
 
-- 
cgit v1.2.3