aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
authorMatej Kosik2015-12-16 16:19:51 +0100
committerMatej Kosik2016-01-11 14:59:26 +0100
commita1aff01d16bad2f44392fd5cb804092e12e558ed (patch)
treebd2a1faf08b1c399171a308cf45bfd46d60ab5c5 /intf
parent78bad016e389cd78635d40281bfefd7136733b7e (diff)
CLEANUP: removing unused field
I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around.
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 8eff327dcd..eaaf2dbb9f 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -75,7 +75,7 @@ type constr_expr =
| CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
| CApp of Loc.t * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
+ | CRecord of Loc.t * (reference * constr_expr) list
| CCases of Loc.t * case_style * constr_expr option *
case_expr list * branch_expr list
| CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *