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
---
 library/global.mli | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'library/global.mli')

diff --git a/library/global.mli b/library/global.mli
index 19d5166257..c2e8ac386c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -23,8 +23,13 @@ val universes : unit -> universes
 val context : unit -> context
 val var_context : unit -> var_context
 
-val push_var : identifier * constr -> unit
-val push_rel : name * constr -> unit
+val push_var_decl : identifier * constr -> unit
+val push_var_def : identifier * constr -> unit
+(*
+val push_var : identifier * constr option * constr -> unit
+val push_rel_decl : name * constr -> unit
+val push_rel_def : name * constr -> unit
+*)
 val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
@@ -32,8 +37,8 @@ val add_constraints : constraints -> unit
 
 val pop_vars : identifier list -> unit
 
-val lookup_var : identifier -> name * typed_type
-val lookup_rel : int -> name * typed_type
+val lookup_var : identifier -> constr option * typed_type
+(*val lookup_rel : int -> name * typed_type*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
-- 
cgit v1.2.3