Ajout option 'Local' à Infix et Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3915 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 18 insertions, 11 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 30e1392364..0c988f315c 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -293,7 +293,7 @@ let exists_notation prec nt =
     !scope_map false 
 
 (* Exportation of scopes *)
-let cache_scope (_,(exp,sc)) =
+let cache_scope (_,(local,sc)) =
   check_scope sc;
   scope_stack := sc :: !scope_stack
 
@@ -301,7 +301,9 @@ let subst_scope (_,subst,sc) = sc
 
 open Libobject
 
-let classify_scope (_,(exp,_ as o)) = if exp then Substitute o else Dispose
+let classify_scope (_,(local,_ as o)) = if local then Dispose else Substitute o
+
+let export_scope (local,_ as x) = if local then None else Some x
 
 let (inScope,outScope) = 
   declare_object {(default_object "SCOPE") with
@@ -309,7 +311,7 @@ let (inScope,outScope) =
       open_function = (fun i o -> if i=1 then cache_scope o);
       subst_function = subst_scope;
       classify_function = classify_scope;
-      export_function = (fun (exp,_ as x) -> if exp then Some x else None) }
+      export_function = export_scope }
 
 let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d24ac4673f..69094507d2 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,7 +31,7 @@ let _ = Summary.declare_summary
 let add_syntax_constant kn c =
   syntax_table := KNmap.add kn c !syntax_table
 
-let load_syntax_constant i ((sp,kn),(c,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
@@ -46,10 +46,14 @@ let open_syntax_constant i ((sp,kn),c) =
 let cache_syntax_constant d =
   load_syntax_constant 1 d
 
-let subst_syntax_constant ((sp,kn),subst,(c,onlyparse)) =
-  (subst_aconstr subst c,onlyparse)
+let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
+  (local,subst_aconstr subst c,onlyparse)
 
-let classify_syntax_constant (_,c) = Substitute c
+let classify_syntax_constant (_,(local,_,_ as o)) =
+  if local then Dispose else Substitute o
+
+let export_syntax_constant (local,_,_ as o) =
+  if local then None else Some o
 
 let (in_syntax_constant, out_syntax_constant) =
   declare_object {(default_object "SYNTAXCONSTANT") with
@@ -58,10 +62,10 @@ let (in_syntax_constant, out_syntax_constant) =
     open_function = open_syntax_constant;
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant;
-    export_function = (fun x -> Some x) } 
+    export_function = export_syntax_constant } 
 
-let declare_syntactic_definition id onlyparse c =
-  let _ = add_leaf id (in_syntax_constant (c,onlyparse)) in ()
+let declare_syntactic_definition local id onlyparse c =
+  let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in ()
 
 let rec set_loc loc _ a =
   map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 87c3e75123..9083158ac4 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -16,7 +16,8 @@ open Rawterm
 
 (* Syntactic definitions. *)
 
-val declare_syntactic_definition : identifier -> bool -> aconstr -> unit
+val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
+  -> unit
 
 val search_syntactic_definition : loc -> kernel_name -> rawconstr