From 8de569861cb8c3ebc697026c43c583a54bae6ce5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Apr 2003 07:58:01 +0000
Subject: Ajout option "Local" à "Open Scope"

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

(limited to 'interp')

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 6a02f284b1..662153f782 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -293,7 +293,7 @@ let exists_notation prec nt =
     !scope_map false 
 
 (* Exportation of scopes *)
-let cache_scope (_,sc) =
+let cache_scope (_,(exp,sc)) =
   check_scope sc;
   scope_stack := sc :: !scope_stack
 
@@ -307,7 +307,7 @@ let (inScope,outScope) =
       open_function = (fun i o -> if i=1 then cache_scope o);
       subst_function = subst_scope;
       classify_function = (fun (_,o) -> Substitute o);
-      export_function = (fun x -> Some x) }
+      export_function = (fun (exp,_ as x) -> if exp then Some x else None) }
 
 let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
 
diff --git a/interp/symbols.mli b/interp/symbols.mli
index c8c844312d..42eedaf81c 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -39,7 +39,7 @@ val declare_scope : scope_name -> unit
 (* Open scope *)
 
 val current_scopes : unit -> scopes
-val open_scope : scope_name -> unit
+val open_scope : bool * scope_name -> unit
 
 (* Declare delimiters for printing *)
 
-- 
cgit v1.2.3