diff options
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 9d6820346..2aec5ed32 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -27,6 +27,13 @@ type intro_pattern_expr = | IntroAnonymous and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) (** Sorts *) |