aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-13 13:11:14 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-13 13:11:14 +0000
commit04f39a03fd7e3845dbe1e8cf5b46cfdf219e6623 (patch)
treec25eca90f235be49cce09c77428f0fb8cb6191ec
parent181646e81cb56e9c799f949e6e42240eace5eb85 (diff)
code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3764 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--toplevel/vernacexpr.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8204a1ead..14c9a295e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -22,11 +22,6 @@ exception ProtectedLoop
exception Drop
exception Quit
-type def_kind = DEFINITION | LET | LOCAL | THEOREM | LETTOP | DECL | REMARK
- | FACT | LEMMA
- | COERCION | LCOERCION | OBJECT | LOBJECT | OBJCOERCION | LOBJCOERCION
- | SUBCLASS | LSUBCLASS
-
open Libnames
open Nametab