aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/misctypes.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 3c6d59ff0c..1452bbc347 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -16,8 +16,6 @@ type patvar = Id.t
(** Introduction patterns *)
-type tuple_flag = bool (* tells pattern list should be list of fixed length *)
-
type 'constr intro_pattern_expr =
| IntroForthcoming of bool
| IntroNaming of intro_pattern_naming_expr