aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b6e2927bb..2d293eacb 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,7 +33,6 @@ 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