From 457e59bd5638c18302caeef281132579bd7dbece Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Sep 1999 14:05:10 +0000
Subject:  - minicoq : definition inductifs; syntaxe a->b  - kernel : bug
 Typing/one_inductive (il fallait chercher l'arite typée dans     
 l'environnement avec lookup_rel et non lookup_var)

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 5ddb8031ed..b02e37b1dd 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -15,8 +15,12 @@ val make_judge : constr -> typed_type -> unsafe_judgment
 
 val j_val_only : unsafe_judgment -> constr
 
+(* If [j] is the judgement $c:t:s$, then [typed_type_of_judgment env j]
+   constructs the typed type $t:s$, while [assumption_of_judgement env j]
+   cosntructs the type type $c:t$, checking that $t$ is a sort. *)
+
 val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
-val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type
+val assumption_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
 
 val relative : 'a unsafe_env -> int -> unsafe_judgment
 
-- 
cgit v1.2.3