From 7ee76fc83bfdec43eca9b9f9c57ea32c64914f3a Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 20 Apr 2001 12:07:01 +0000
Subject: un typage sûr pour Goal et Check

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

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f72712cc8e..d1ca1a52fa 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -166,12 +166,11 @@ let execute_type env constr =
   let (j,cst) = execute env constr in
   (type_judgment env Evd.empty j, cst)
 
+(* Renaming for the following. *)
 
-(* Exported machines. *)
+let safe_infer = execute
 
-let safe_infer env constr = execute env constr
-
-let safe_infer_type env constr = execute_type env constr
+let safe_infer_type = execute_type
 
 (* Typing of several terms. *)
 
@@ -471,3 +470,11 @@ let import = import
 
 let env_of_safe_env e = e
 
+(* Exported typing functions *)
+
+let typing env c = 
+  let (j,cst) = safe_infer env c in
+  let _ = add_constraints cst env in
+  j
+
+let typing_in_unsafe_env = typing
-- 
cgit v1.2.3