aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/miscops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/miscops.ml')
-rw-r--r--pretyping/miscops.ml10
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"