diff options
Diffstat (limited to 'pretyping/miscops.ml')
| -rw-r--r-- | pretyping/miscops.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 2528d57f3..0f659f1b6 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -10,6 +10,8 @@ open Misctypes open Pp open Nameops +(** Mapping [cast_type] *) + let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) @@ -41,3 +43,11 @@ and pr_or_and_intro_pattern = function str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) 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" |