From a807069e370eb1a8f4d7f4e8b72449017a68d891 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 11 Oct 2004 10:25:50 +0000
Subject: Suppression IsConjecture redondant avec Conjectural

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6198 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/decl_kinds.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'library')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index bec9ab7c6..66b1bb072 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -61,7 +61,6 @@ type local_theorem_kind = LocalStatement
 type 'a mathematical_kind =
   | IsAssumption of type_as_formula_kind
   | IsDefinition
-  | IsConjecture
   | IsProof of 'a
 
 type global_kind = theorem_kind mathematical_kind
-- 
cgit v1.2.3