diff options
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) = |