From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 interp/notation.ml | 28 +++++++++++++---------------
 1 file changed, 13 insertions(+), 15 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 98a199ad..9e83b860 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 10893 2008-05-07 09:20:43Z herbelin $ *)
+(* $Id: notation.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (*i*)
 open Util
@@ -78,7 +78,7 @@ let declare_scope scope =
 
 let find_scope scope =
   try Gmap.find scope !scope_map
-  with Not_found -> error ("Scope "^scope^" is not declared")
+  with Not_found -> error ("Scope "^scope^" is not declared.")
 
 let check_scope sc = let _ = find_scope sc in ()
 
@@ -159,7 +159,7 @@ let find_delimiters_scope loc key =
   try Gmap.find key !delimiters_map
   with Not_found -> 
     user_err_loc 
-    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
 
 (* Uninterpretation tables *)
 
@@ -251,7 +251,7 @@ let check_required_module loc sc (sp,d) =
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret in "^sc^" without requiring first module "
-    ^(list_last d)))
+    ^(list_last d)^"."))
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -348,7 +348,7 @@ let interp_prim_token_gen g loc p local_scopes =
     user_err_loc (loc,"interp_prim_token",
     (match p with
       | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
-      | String s -> str "No interpretation for string " ++ qs s))
+      | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token =
   interp_prim_token_gen (fun x -> x)
@@ -361,7 +361,7 @@ let rec interp_notation loc ntn local_scopes =
   try find_interpretation (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
-    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
+    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
 let uninterp_notations c =
   Gmapl.find (rawconstr_key c) !notations_key_table
@@ -464,10 +464,10 @@ let subst_arguments_scope (_,subst,(req,r,scl)) =
   (ArgsScopeNoDischarge,fst (subst_global subst r),scl)
 
 let discharge_arguments_scope (_,(req,r,l)) =
-  if req = ArgsScopeNoDischarge then None
-  else Some (req,pop_global_reference r,l)
+  if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
+  else Some (req,Lib.discharge_global r,l)
 
-let rebuild_arguments_scope (_,(req,r,l)) =
+let rebuild_arguments_scope (req,r,l) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
@@ -493,8 +493,7 @@ let declare_arguments_scope_gen req r scl =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
 
 let declare_arguments_scope local ref scl =
-  let req =
-    if local or isVarRef ref then ArgsScopeNoDischarge else ArgsScopeManual in
+  let req = if local then ArgsScopeNoDischarge else ArgsScopeManual in
   declare_arguments_scope_gen req ref scl
 
 let find_arguments_scope r =
@@ -503,8 +502,7 @@ let find_arguments_scope r =
 
 let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
-  let req = if isVarRef ref then ArgsScopeNoDischarge else ArgsScopeAuto in
-  declare_arguments_scope_gen req ref (compute_arguments_scope t)
+  declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t)
 
 (********************************)
 (* Encoding notations as string *)
@@ -627,12 +625,12 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
   | _ -> None
 
 let error_ambiguous_notation loc _ntn =
-  user_err_loc (loc,"",str "Ambiguous notation")
+  user_err_loc (loc,"",str "Ambiguous notation.")
 
 let error_notation_not_reference loc ntn =
   user_err_loc (loc,"",
     str "Unable to interpret " ++ quote (str ntn) ++
-    str " as a reference")
+    str " as a reference.")
 
 let interp_notation_as_global_reference loc test ntn =
   let ntns = browse_notation true ntn !scope_map in
-- 
cgit v1.2.3