summaryrefslogtreecommitdiff
path: root/proofs/decl_expr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/decl_expr.mli')
-rw-r--r--proofs/decl_expr.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index a8b7c0d6..22752eda 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: decl_expr.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
open Names
open Util
@@ -18,7 +18,6 @@ type 'it statement =
type thesis_kind =
Plain
- | Sub of int
| For of identifier
type 'this or_thesis =