From a807069e370eb1a8f4d7f4e8b72449017a68d891 Mon Sep 17 00:00:00 2001
From: herbelin
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
---
 contrib/xml/xmlcommand.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'contrib/xml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 2157dab56f..ba9e87e0ba 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -455,7 +455,6 @@ let kind_of_variable id =
     | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
     | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
     | DK.IsDefinition -> "VARIABLE","LocalDefinition"
-    | DK.IsConjecture -> "VARIABLE","Conjecture"
     | DK.IsProof DK.LocalStatement -> "VARIABLE","LocalFact"
 ;;
 
@@ -466,7 +465,6 @@ let kind_of_constant kn =
     | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
     | DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
     | DK.IsDefinition -> "DEFINITION","Definition"
-    | DK.IsConjecture -> "THEOREM","Conjecture"
     | DK.IsProof thm -> "THEOREM",kind_of_theorem thm
 ;;
 
-- 
cgit v1.2.3