diff options
Diffstat (limited to 'proofs/miscprint.ml')
| -rw-r--r-- | proofs/miscprint.ml | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index 1a63ff67..ec17b807 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -10,7 +10,7 @@ open Pp open Names -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with | IntroNaming p -> pr_intro_pattern_naming p | IntroAction p -> pr_intro_pattern_action prc p -and pr_intro_pattern_naming = function +and pr_intro_pattern_naming = let open Namegen in function | IntroIdentifier id -> Id.print id | IntroFresh id -> str "?" ++ Id.print id | IntroAnonymous -> str "?" @@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - (** Printing of bindings *) let pr_binding prc = let open CAst in function | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) |