diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 00:07:26 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
commit | 368a25e4ef14512b00f5799e26c3f615bc540201 (patch) | |
tree | 29602372307ff70f2a7b06f0a27609a73caa5666 /proofs/miscprint.ml | |
parent | 36a98d55576ebdb106a55c3bd682961da8d77dee (diff) |
[api] Misctypes removal: several moves:
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
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 1a63ff673..ec17b8076 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) |