aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/decl_expr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/decl_expr.mli')
-rw-r--r--proofs/decl_expr.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 1c5cc0e74..d02060fc0 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -18,7 +18,6 @@ type 'it statement =
type thesis_kind =
Plain
- | Sub of int
| For of identifier
type 'this or_thesis =