aboutsummaryrefslogtreecommitdiff
path: root/proofs/decl_expr.mli
diff options
context:
space:
mode:
authorcorbinea2007-04-26 08:54:28 +0000
committercorbinea2007-04-26 08:54:28 +0000
commitea1eaa9b152b73652f417e02bd469e5b289cec47 (patch)
tree4d654ad1434bac0781eb4f3e6f1505c3895df4ba /proofs/decl_expr.mli
parent40425048feff138e6c67555c7ee94142452d1cae (diff)
fin des conclusions multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1c5cc0e746..d02060fc0a 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 =