From 3afaf3dde673d77cacaabc354f008dfbe49a7cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:39:23 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.mli | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5f6b9b073e..6d8c80bd0d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -26,8 +26,13 @@ val universes : safe_environment -> universes
 val context : safe_environment -> context
 val var_context : safe_environment -> var_context
 
-val push_var : identifier * constr -> safe_environment -> safe_environment
-val push_rel : name * constr -> safe_environment -> safe_environment
+val push_var_decl : identifier * constr -> safe_environment -> safe_environment
+val push_var_def : identifier * constr -> safe_environment -> safe_environment
+(*
+val push_rel_decl : name * constr -> safe_environment -> safe_environment
+val push_rel_def : name * constr -> safe_environment -> safe_environment
+*)
+
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
 val add_lazy_constant : 
@@ -42,8 +47,10 @@ val add_constraints : constraints -> safe_environment -> safe_environment
 
 val pop_vars : identifier list -> safe_environment -> safe_environment
 
-val lookup_var : identifier -> safe_environment -> name * typed_type
+val lookup_var : identifier -> safe_environment -> constr option * typed_type
+(*
 val lookup_rel : int -> safe_environment -> name * typed_type
+*)
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
 val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
-- 
cgit v1.2.3