diff options
| author | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
| commit | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (patch) | |
| tree | 39f0c957c4ea02e6976299b4183b6bcfa8ea9f7a /printing | |
| parent | 48ec42bb91b8c0fb4d5930e62e29a408de594482 (diff) | |
| parent | fca82378cd2824534383f1f5bc09d08fade1dc17 (diff) | |
Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 83c8757070..89117caf4b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -145,7 +145,7 @@ open Pputils | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -508,7 +508,7 @@ open Pputils | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,l,gopt) -> - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -1122,7 +1122,7 @@ open Pputils | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in + | Some i -> Goal_select.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) @@ -1176,7 +1176,8 @@ open Pputils | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) | VernacBullet b -> - return (begin match b with + (* XXX: Redundant with Proof_bullet.print *) + return (let open Proof_bullet in begin match b with | Dash n -> str (String.make n '-') | Star n -> str (String.make n '*') | Plus n -> str (String.make n '+') @@ -1184,7 +1185,7 @@ open Pputils | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") + return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") |