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.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'library/global.ml')

diff --git a/library/global.ml b/library/global.ml
index cf3d88ca93..a37863a78f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -30,8 +30,12 @@ let universes () = universes !global_env
 let context () = context !global_env
 let var_context () = var_context !global_env
 
-let push_var idc = global_env := push_var idc !global_env
-let push_rel nac = global_env := push_rel nac !global_env
+let push_var_def idc = global_env := push_var_def idc !global_env
+let push_var_decl idc = global_env := push_var_decl idc !global_env
+(*
+let push_rel_def nac = global_env := push_rel nac !global_env
+let push_rel_decl nac = global_env := push_rel nac !global_env
+*)
 let add_constant sp ce = global_env := add_constant sp ce !global_env
 let add_parameter sp c = global_env := add_parameter sp c !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
@@ -40,7 +44,9 @@ let add_constraints c = global_env := add_constraints c !global_env
 let pop_vars ids = global_env := pop_vars ids !global_env
 
 let lookup_var id = lookup_var id !global_env
+(*
 let lookup_rel n = lookup_rel n !global_env
+*)
 let lookup_constant sp = lookup_constant sp !global_env
 let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
-- 
cgit v1.2.3