From 32170384190168856efeac5bcf90edf1170b54d6 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 29 May 2002 10:48:37 +0000
Subject: Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques
 et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6980c9759..94d4e0844 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -89,3 +89,7 @@ val judge_of_case : env -> case_info
 (* Typecheck general fixpoint (not checking guard conditions) *)
 val type_fixpoint : env -> name array -> types array 
     -> unsafe_judgment array -> constraints
+
+(* Kernel safe typing but applicable to partial proofs *)
+val typing : env -> constr -> unsafe_judgment
+
-- 
cgit v1.2.3