From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 interp/notation.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp/notation.ml')

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) =
-- 
cgit v1.2.3