Ajout d'un choix 'onlyparse'

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

4 files changed, 14 insertions, 10 deletions

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index eef20a7b16..d24ac4673f 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,13 +31,14 @@ 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) =
+let load_syntax_constant i ((sp,kn),(c,onlyparse)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn c;
   Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
-  Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
+  if not onlyparse then
+    Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
 let open_syntax_constant i ((sp,kn),c) =
   Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
@@ -45,8 +46,8 @@ 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) =
-  subst_aconstr subst c
+let subst_syntax_constant ((sp,kn),subst,(c,onlyparse)) =
+  (subst_aconstr subst c,onlyparse)
 
 let classify_syntax_constant (_,c) = Substitute c
 
@@ -59,8 +60,8 @@ let (in_syntax_constant, out_syntax_constant) =
     classify_function = classify_syntax_constant;
     export_function = (fun x -> Some x) } 
 
-let declare_syntactic_definition id c =
-  let _ = add_leaf id (in_syntax_constant c) in ()
+let declare_syntactic_definition id onlyparse c =
+  let _ = add_leaf id (in_syntax_constant (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 f4600d8dbf..87c3e75123 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -16,7 +16,7 @@ open Rawterm
 
 (* Syntactic definitions. *)
 
-val declare_syntactic_definition : identifier -> aconstr -> unit
+val declare_syntactic_definition : identifier -> bool -> aconstr -> unit
 
 val search_syntactic_definition : loc -> kernel_name -> rawconstr
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8279c14527..63c7cce93c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -121,7 +121,8 @@ let declare_definition ident local bl red_option c typopt =
 
 let syntax_definition ident c =
   let c = snd (interp_aconstr [] c) in 
-  Syntax_def.declare_syntactic_definition ident c;
+  let onlyparse = !Options.v7_only in
+  Syntax_def.declare_syntactic_definition ident onlyparse c;
   if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
 
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 36734041ab..af9de6b434 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -681,11 +681,13 @@ let add_notation_in_scope df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
 let add_notation df a modifiers mv8 sc =
   let toks = split df in
   match toks with 
-    | [String x] when quote(strip x) = x & modifiers = [] ->
+    | [String x] when quote(strip x) = x
+	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
         (* Means a Syntactic Definition *)
         let ident = id_of_string (strip x) in
 	let c = snd (interp_aconstr [] a) in
-        Syntax_def.declare_syntactic_definition ident c
+	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
+        Syntax_def.declare_syntactic_definition ident onlyparse c
     | _ ->
         add_notation_in_scope
           df a (interp_notation_modifiers modifiers)