diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /interp/notation.ml | |
parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index fe9d8b6d..8bf7ba21 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *) (*i*) open Util @@ -113,7 +113,7 @@ let subst_scope (subst,sc) = sc open Libobject -let discharge_scope (local,_,_ as o) = +let discharge_scope (_,(local,_,_ as o)) = if local then None else Some o let classify_scope (local,_,_ as o) = @@ -124,6 +124,7 @@ let (inScope,outScope) = cache_function = cache_scope; open_function = open_scope; subst_function = subst_scope; + discharge_function = discharge_scope; classify_function = classify_scope } let open_close_scope (local,opening,sc) = |