From 1e4c9c6dd74162c5fd75de59f1cab117e458e8de Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Sep 2001 15:01:54 +0000
Subject: Mécanisme pour faire remonter les contraintes de typage sur les
 variables de section au niveau du discharge, sans avoir à garder tout
 l'environnement de la section

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

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 482be2fb99..e8ed6ca32e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,4 +161,5 @@ let cook_constant env r =
   let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
   let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
   let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in
-  abstract_constant r.d_abstract hyps (body,typ)
+  let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
+  (body, typ, cb.const_constraints)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index d9b564835b..db2ba15516 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -12,6 +12,7 @@ open Names
 open Term
 open Declarations
 open Environ
+open Univ
 
 (*s Cooking the constants. *)
 
@@ -32,7 +33,7 @@ type recipe = {
   d_abstract : identifier list;
   d_modlist : work_list }
 
-val cook_constant : env -> recipe -> constr option * constr
+val cook_constant : env -> recipe -> constr option * constr * constraints
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 102fbb228e..ff1a8131d6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -38,6 +38,13 @@ val push_named_assum :
 val push_named_def :
   identifier * constr -> safe_environment -> safe_environment
 
+val check_and_push_named_assum :
+  identifier * constr -> safe_environment ->
+    (constr option * types * constraints) * safe_environment
+val check_and_push_named_def :
+  identifier * constr -> safe_environment -> 
+    (constr option * types * constraints) * safe_environment
+
 type local_names = (identifier * variable_path) list
 
 val add_parameter :
-- 
cgit v1.2.3