diff options
| author | herbelin | 2003-04-08 07:58:01 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-08 07:58:01 +0000 |
| commit | 8de569861cb8c3ebc697026c43c583a54bae6ce5 (patch) | |
| tree | 282ba082d2eafe3ea5fa4c80e67be6f03f94000f /interp | |
| parent | a330ee4a6e399824294887cbb1f496c7ed5a8208 (diff) | |
Ajout option "Local" à "Open Scope"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/symbols.ml | 4 | ||||
| -rw-r--r-- | interp/symbols.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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 *) |