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 ---
 kernel/safe_typing.mli | 14 ++++----------
 2 files changed, 4 insertions(+), 13 deletions(-)

(limited to 'kernel')

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
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 4ed912d4cf..5f6b9b073e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -53,16 +53,17 @@ val import : compiled_env -> safe_environment -> safe_environment
 
 val env_of_safe_env : safe_environment -> env
 
-(*i For debug
-(*s Typing without information. *)
+
+(*s Typing judgments (only used in minicoq). *)
+
 type judgment
 
 val j_val : judgment -> constr
 val j_type : judgment -> constr
 
 val safe_machine : safe_environment -> constr -> judgment * constraints
-val safe_machine_type : safe_environment -> constr -> typed_type * constraints
 
+(*i For debug
 val fix_machine : safe_environment -> constr -> judgment * constraints
 val fix_machine_type : safe_environment -> constr -> typed_type * constraints
 
@@ -71,14 +72,7 @@ val unsafe_machine_type : safe_environment -> constr -> typed_type * constraints
 
 val type_of : safe_environment -> constr -> constr
 
-(*i obsolète 
 val type_of_type : safe_environment -> constr -> constr
 val unsafe_type_of : safe_environment -> constr -> constr
 i*)
 
-
-(*s Typing with information (extraction). *)
-
-type information = Logic | Inf of judgment
-i*)
-
-- 
cgit v1.2.3