From ba18968685be05d370bb0a82fc3f5e403cdced9f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 21 Jul 2000 17:31:35 +0000
Subject: retablissement minicoq (pour Jacek)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 48692008cb..d4b610a8e8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -463,6 +463,3 @@ let import = import
 
 let env_of_safe_env e = e
 
-(*s Machines with information. *)
-
-type information = Logic | Inf of unsafe_judgment
-- 
cgit v1.2.3