diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 396add2646..42af0f2e61 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -895,9 +895,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())) ) |