aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 0064d238d..b6e2927bb 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,6 +33,7 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
+ | ARecord of aconstr option * (identifier * aconstr) list
| ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
(cases_pattern list * aconstr) list
@@ -133,6 +134,7 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
+ | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list