diff options
| author | ppedrot | 2013-08-01 14:26:02 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-01 14:26:02 +0000 |
| commit | 0f999f0447e92343be9eed116e33df3149339b82 (patch) | |
| tree | 2ced4e2c3d615b2c0955d4c2e9b3f40c2db85334 /printing | |
| parent | 1ce0550e04870a5a93d464bab8c2be6fb5d2702d (diff) | |
Granting bug #3098: adding priority to Existing Instances.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16645 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3c4f25880b..3e6fa48615 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -381,6 +381,10 @@ let pr_statement head (id,(bl,c,guard)) = pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) +let pr_priority = function +| None -> mt () +| Some i -> spc () ++ str "|" ++ spc () ++ int i + (**************************************) (* Pretty printer for vernac commands *) (**************************************) @@ -714,7 +718,7 @@ let rec pr_vernac = function Anonymous -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - pr_constr cl ++ spc () ++ + pr_constr cl ++ pr_priority pri ++ (match props with | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) @@ -724,10 +728,10 @@ let rec pr_vernac = function str"Context" ++ spc () ++ pr_and_type_binders_arg l) - | VernacDeclareInstances ids -> + | VernacDeclareInstances (ids, pri) -> hov 1 ( str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++ - spc () ++ prlist_with_sep spc pr_reference ids) + spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) | VernacDeclareClass id -> hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id) |