Réutilisation de VernacSyntacticDefinition pour différencier "Notation id := c"

de "Notation "'id'" := c"


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

10 files changed, 26 insertions, 38 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0e6fc29980..f19404e106 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1798,8 +1798,10 @@ let rec xlate_vernac =
 	     xlate_sort sort) in
         CT_ind_scheme
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
-   | VernacSyntacticDefinition ((_,id), c, nopt) ->
-         CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt nopt)
+   | VernacSyntacticDefinition (id, c, false, _) ->
+       CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
+   | VernacSyntacticDefinition (id, c, true, _) ->
+       xlate_error "TODO: Local abbreviations"
    | VernacRequire (impexp, spec, id::idl) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec in
       CT_require (ct_impexp, ct_spec, 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index bd505088c8..6476851637 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -337,10 +337,9 @@ GEXTEND Gram
 (*
 	     VernacDistfix (local,a,n,s,p,sc)
 *)
-     | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr;
-	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
-	       | -> [] ] ->
-	 VernacNotation (local,c,Some("'"^s^"'",l),None,None)
+     | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
+         b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
+	 VernacSyntacticDefinition (id,c,local,b)
      | IDENT "Notation"; local = locality; s = lstring; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ];
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d79b3ec3a8..ad3862388e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -418,14 +418,14 @@ GEXTEND Gram
          n = OPT [ "|"; n = natural -> n ] ->
 	   VernacSyntacticDefinition (id,c,n)
 *)
-      | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr;
+      | IDENT "Syntactic"; "Definition"; id = ident; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   let c = match n with
 	     | Some n ->
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
 		 CApp (loc,(None,c),l)
 	     | None -> c in
-	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
+	   VernacSyntacticDefinition (id,c,false,true)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  let l = List.map (fun n -> ExplByPos n) l in
 	  VernacDeclareImplicits (qid,Some l)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index cf89300bba..d62d40d33b 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -675,10 +675,9 @@ GEXTEND Gram
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacInfix (local,(op,modl),p,Some(op,modl),sc)
-     | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr;
-	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
-	       | -> [] ] ->
-	 VernacNotation (local,c,Some("'"^s^"'",l),Some("'"^s^"'",l),None)
+     | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
+	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
+           VernacSyntacticDefinition (id,c,local,b)
      | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 8c1ff3211e..6b3f9f8c02 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -308,7 +308,8 @@ let print_inductive sp = (print_mutual sp)
 let print_syntactic_def sep kn =
   let qid = Nametab.shortest_qualid_of_syndef kn in
   let c = Syntax_def.search_syntactic_definition dummy_loc kn in 
-  (str"Syntactic Definition " ++ pr_qualid qid ++ str sep ++ 
+  (str (if !Options.v7 then "Syntactic Definition " else "Notation ")
+   ++ pr_qualid qid ++ str sep ++ 
   Constrextern.without_symbols pr_rawterm c ++ fnl ())
 
 let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
@@ -419,7 +420,7 @@ let print_name ref =
   | Term (IndRef (sp,_)) -> print_inductive sp
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
   | Term (VarRef sp) -> print_section_variable sp
-  | Syntactic kn -> print_syntactic_def " = " kn
+  | Syntactic kn -> print_syntactic_def " := " kn
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
   | Dir _ -> mt ()
   | ModuleType (_,kn) -> print_modtype kn
@@ -481,7 +482,7 @@ let print_about ref =
   let k = locate_any_name ref in
   begin match k with
   | Term ref -> print_ref false ref ++ print_name_infos ref
-  | Syntactic kn -> print_syntactic_def " = " kn
+  | Syntactic kn -> print_syntactic_def " := " kn
   | Dir _ | ModuleType _ | Undefined _ -> mt () end
   ++
   hov 0 (str "Expands to: " ++ pr_located_qualid k)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ea38340cea..5c0b5818c5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -135,12 +135,10 @@ let declare_definition ident (local,_) bl red_option c typopt hook =
         declare_global_definition ident ce' local in
   hook local r
 
-let syntax_definition ident c =
-  let c = snd (interp_aconstr [] [] c) in 
-  let onlyparse = !Options.v7_only in
-  Syntax_def.declare_syntactic_definition false ident onlyparse c;
-  if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
-
+let syntax_definition ident c local onlyparse =
+  let c = snd (interp_aconstr [] [] c) in
+  let onlyparse = !Options.v7_only or onlyparse in
+  Syntax_def.declare_syntactic_definition local ident onlyparse c
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index db5ab27b09..c2db70dafc 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -33,7 +33,7 @@ val declare_definition : identifier -> definition_kind ->
   local_binder list -> Tacred.red_expr option -> constr_expr ->
     constr_expr option -> declaration_hook -> unit
 
-val syntax_definition : identifier -> constr_expr -> unit
+val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 538c7563a3..a50339c6e9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1111,14 +1111,6 @@ let add_notation local c dfmod mv8 sc =
   | Some (df,modifiers) ->
   let toks = split_notation_string df in
   match toks with 
-    | [String x] when is_quoted_ident x 
-	(* This is an ident that can be qualified: a syntactic definition *)
-	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
-        (* Means a Syntactic Definition *)
-        let ident = id_of_string (unquote_notation_token x) in
-	let c = snd (interp_aconstr [] [] c) in
-	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
-        Syntax_def.declare_syntactic_definition local ident onlyparse c
     | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
 	(* This is a ident to be declared as a rule *)
         add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc toks
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 91c23fb7a3..33b1952c7d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -659,12 +659,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 
 let vernac_hints = Auto.add_hints
 
-let vernac_syntactic_definition id c = function
-  | None -> syntax_definition id c
-  | Some n ->
-      let l = list_tabulate (fun _ -> (CHole (dummy_loc),None)) n in
-      let c = CApp (dummy_loc,(None,c),l) in
-      syntax_definition id c
+let vernac_syntactic_definition = Command.syntax_definition 
 
 let vernac_declare_implicits locqid = function
   | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps
@@ -1197,7 +1192,7 @@ let interp c = match c with
   (* Commands *)
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
-  | VernacSyntacticDefinition ((_,id),c,n) -> vernac_syntactic_definition id c n
+  | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 7b1203e57b..64b6bb7426 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -132,6 +132,7 @@ type coercion_flag  = bool (* true = AddCoercion;   false = NoCoercion     *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
 type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
+type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 
 type sort_expr = Rawterm.rawsort
 
@@ -245,7 +246,8 @@ type vernac_expr =
   | VernacDeclareTacticDefinition of
       rec_flag * (lident * raw_tactic_expr) list
   | VernacHints of locality_flag * lstring list * hints
-  | VernacSyntacticDefinition of lident * constr_expr * int option
+  | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
+      onlyparsing_flag
   | VernacDeclareImplicits of lreference * explicitation list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list