From 19d21ec59b69a7bd5a8e4e77794e85fed6b48d39 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 30 Aug 1999 07:27:52 +0000
Subject: un petit effort de presentation dans les interfaces

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 34d8898971..15b2ca821d 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Constant
@@ -8,6 +9,12 @@ open Inductive
 open Evd
 open Univ
 open Sign
+(*i*)
+
+(* Unsafe environments. We define here a datatype for environments. 
+   Since typing is not yet defined, it is not possible to check the
+   informations added in environments, and that is what we speak here
+   of ``unsafe'' environments. *)
 
 type 'a unsafe_env
 
@@ -50,6 +57,10 @@ val is_existential : constr -> bool
 
 val mind_nparams : 'a unsafe_env -> constr -> int
 
+(*s Unsafe judgments. We introduce here the pre-type of judgments, which is
+  actually only a datatype to store a term with its type and the type of its
+  type. *)
+
 type unsafe_judgment = { 
   uj_val : constr;
   uj_type : constr;
-- 
cgit v1.2.3