From 79ac780518b797b9e2181ef3993cb08c202b130a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 19 Nov 2001 10:38:25 +0000
Subject: Mise en place d'une méthode directe pour indiquer le type des
 déclarations à toplevel plutôt que de passer par mkCast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml  | 9 +++++++--
 kernel/safe_typing.mli | 2 +-
 2 files changed, 8 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c770e0237a..fdb7c0d0c1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -38,10 +38,15 @@ let empty_environment = empty_env
 (* Insertion of variables (named and de Bruijn'ed). They are now typed before
    being added to the environment. *)
 
-let push_rel_or_named_def push (id,b) env =
+let push_rel_or_named_def push (id,b,topt) env =
   let (j,cst) = safe_infer env b in
+  let (t,cst) = match topt with
+    | None -> j.uj_type, cst
+    | Some t -> 
+	let (jt,cstt) = safe_infer_type env t in
+	jt.utj_val, Constraint.union cst cstt in
   let env' = add_constraints cst env in
-  let env'' = push (id,Some j.uj_val,j.uj_type) env' in
+  let env'' = push (id,Some j.uj_val,t) env' in
   (cst,env'')
 
 let push_named_def = push_rel_or_named_def push_named_decl
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5f6697b4eb..36c2bbb23a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -30,7 +30,7 @@ val push_named_assum :
   identifier * types -> safe_environment ->
     Univ.constraints * safe_environment
 val push_named_def :
-  identifier * constr -> safe_environment ->
+  identifier * constr * types option -> safe_environment ->
     Univ.constraints * safe_environment
 val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
-- 
cgit v1.2.3