Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

3 files changed, 49 insertions, 15 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d09430dc..4550518d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
+(* $Id: constrintern.ml 9611 2007-02-07 15:51:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -292,6 +292,12 @@ let intern_qualid loc qid =
   with Not_found ->
     error_global_not_found_loc loc qid
 
+(* Rule out section vars since these should have been found by intern_var *)
+let intern_non_secvar_qualid loc qid =
+  match intern_qualid loc qid with
+    | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid
+    | r -> r
+
 let intern_inductive r =
   let loc,qid = qualid_of_reference r in
   try match Nametab.extended_locate qid with
@@ -312,7 +318,8 @@ let intern_reference env lvar = function
   | Ident (loc, id) ->
       try intern_var env lvar loc id
       with Not_found -> 
-      try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id))
+      let qid = make_short_qualid id in
+      try find_appl_head_data lvar (intern_non_secvar_qualid loc qid)
       with e ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar then RVar (loc,id), [], [], []
diff --git a/interp/notation.ml b/interp/notation.ml
index 5b6692e9..7d70b296 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 9258 2006-10-23 07:15:04Z courtieu $ *)
+(* $Id: notation.ml 9481 2007-01-11 19:17:56Z herbelin $ *)
 
 (*i*)
 open Util
@@ -446,19 +446,36 @@ let rec compute_arguments_scope t =
 
 let arguments_scope = ref Refmap.empty
 
-let load_arguments_scope _ (_,(r,scl)) =
+type arguments_scope_discharge_request =
+  | ArgsScopeAuto
+  | ArgsScopeManual
+  | ArgsScopeNoDischarge
+
+let load_arguments_scope _ (_,(_,r,scl)) =
   List.iter (option_iter check_scope) scl;
   arguments_scope := Refmap.add r scl !arguments_scope
 
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl)
-
-let discharge_arguments_scope (r,_) =
-  match r with
-    | VarRef _ -> None
-    | _ -> Some (r,compute_arguments_scope (Global.type_of_global r))
+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)
+
+let rebuild_arguments_scope (req,r,l) =
+  match req with
+    | ArgsScopeNoDischarge -> assert false
+    | ArgsScopeAuto ->
+	(req,r,compute_arguments_scope (Global.type_of_global r))
+    | ArgsScopeManual ->
+	(* Add to the manually given scopes the one found automatically
+           for the extra parameters of the section *)
+	let l' = compute_arguments_scope (Global.type_of_global r) in
+	let l1,_ = list_chop (List.length l' - List.length l) l' in
+	(req,r,l1@l)
 
 let (inArgumentsScope,outArgumentsScope) = 
   declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -466,10 +483,17 @@ let (inArgumentsScope,outArgumentsScope) =
       load_function = load_arguments_scope;
       subst_function = subst_arguments_scope;
       classify_function = (fun (_,o) -> Substitute o);
+      discharge_function = discharge_arguments_scope;
+      rebuild_function = rebuild_arguments_scope;
       export_function = (fun x -> Some x) }
 
-let declare_arguments_scope r scl =
-  Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+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
+  declare_arguments_scope_gen req ref scl
 
 let find_arguments_scope r =
   try Refmap.find r !arguments_scope
@@ -477,7 +501,8 @@ let find_arguments_scope r =
 
 let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
-  declare_arguments_scope ref (compute_arguments_scope t)
+  let req = if isVarRef ref then ArgsScopeNoDischarge else ArgsScopeAuto in
+  declare_arguments_scope_gen req ref (compute_arguments_scope t)
 
 (********************************)
 (* Encoding notations as string *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 840274c5..7be1f9fe 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: notation.mli 9208 2006-10-05 07:45:01Z herbelin $ i*)
+(*i $Id: notation.mli 9481 2007-01-11 19:17:56Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -135,7 +135,9 @@ val exists_notation_in_scope : scope_name option -> notation ->
       interpretation -> bool
 
 (* Declares and looks for scopes associated to arguments of a global ref *)
-val declare_arguments_scope: global_reference -> scope_name option list -> unit
+val declare_arguments_scope : 
+  bool (* true=local *) -> global_reference -> scope_name option list -> unit
+
 val find_arguments_scope : global_reference -> scope_name option list
 
 val declare_class_scope : scope_name -> Classops.cl_typ -> unit