Added support for option Local (at module level) in Tactic Notation.

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

9 files changed, 28 insertions, 16 deletions

diff --git a/CHANGES b/CHANGES
index 8f3c3eb89..3719481de 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,7 @@ Tactics
   record-like inductive types, superseding the old version of "tauto".
 - Similarly, "intuition" has been made more uniform and, where it now
   fails, "dintuition" can be used. (possible source of incompatibilities)
+- Tactic notations can now be defined locally to a module (use "Local" prefix).
 
 Program
 
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index d0512c852..1bae52617 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -168,7 +168,7 @@
 \newcommand{\flag}{\nterm{flag}}
 \newcommand{\form}{\nterm{form}}
 \newcommand{\entry}{\nterm{entry}} 
-\newcommand{\proditem}{\nterm{production\_item}}
+\newcommand{\proditem}{\nterm{prod\_item}}
 \newcommand{\taclevel}{\nterm{tactic\_level}}
 \newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} 
 \newcommand{\scope}{\nterm{scope}} 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index d1e225636..be10ac4bf 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -1089,11 +1089,11 @@ syntax
 
 \noindent
 \begin{tabular}{lcl}
-{\sentence} & ::= & \texttt{Tactic Notation} \zeroone{\taclevel} \nelist{\proditem}{} \\
+{\sentence} & ::= & \zeroone{\tt Local} \texttt{Tactic Notation} \zeroone{\taclevel} \sequence{\proditem}{} \\
 & & \texttt{:= {\tac} .}\\
 {\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ 
 {\taclevel} & ::= & {\tt (at level} {\naturalnumber}{\tt )} \\
-{\tacargtype} & ::= &
+{\tacargtype}\!\! & ::= &
 %{\tt preident} $|$
 {\tt ident} $|$
 {\tt simple\_intropattern} $|$
@@ -1171,6 +1171,10 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is
 either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
 {\tt\small int\_or\_var}.
 
+Tactic notations do not survive the end of sections. They survive
+modules unless the command {\tt Local Tactic Notation} is used instead
+of {\tt Tactic Notation}.
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 04b8f0d14..dfa03a4d7 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -215,7 +215,8 @@ type vernac_expr =
   | VernacFail of vernac_expr
 
   (* Syntax *)
-  | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr
+  | VernacTacticNotation of
+      locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr
   | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * string
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 97d8196de..e9b91dbbf 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -998,7 +998,7 @@ GEXTEND Gram
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
-         -> VernacTacticNotation (n,pil,t)
+         -> VernacTacticNotation (use_module_locality(),n,pil,t)
 
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index bdf5a26ef..70094b48c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -497,7 +497,8 @@ let rec pr_vernac = function
   | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
 
   (* Syntax *)
-  | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)
+  | VernacTacticNotation (local,n,r,e) ->
+      pr_locality local ++ pr_grammar_tactic_rule n ("",r,e)
   | VernacOpenCloseScope (local,opening,sc) ->
       pr_section_locality local ++
       str (if opening then "Open " else "Close ") ++
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fe362bee3..2e7b37db7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -65,18 +65,22 @@ let rec make_tags = function
   | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
   | [] -> []
 
-let cache_tactic_notation (_,(pa,pp)) =
+let cache_tactic_notation (_,(local,pa,pp)) =
   Egramcoq.extend_grammar (Egramcoq.TacticGrammar pa);
   Pptactic.declare_extra_tactic_pprule pp
 
 let subst_tactic_parule subst (key,n,p,(d,tac)) =
   (key,n,p,(d,Tacinterp.subst_tactic subst tac))
 
-let subst_tactic_notation (subst,(pa,pp)) =
-  (subst_tactic_parule subst pa,pp)
+let subst_tactic_notation (subst,(local,pa,pp)) =
+  (local,subst_tactic_parule subst pa,pp)
+
+let classify_tactic_notation (local,_,_ as o) =
+  if local then Dispose else Substitute o
 
 type tactic_grammar_obj =
-    (string * int * grammar_prod_item list *
+    locality_flag
+    * (string * int * grammar_prod_item list *
        (dir_path * Tacexpr.glob_tactic_expr))
     * (string * Genarg.argument_type list * (int * Pptactic.grammar_terminals))
 
@@ -85,7 +89,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
        open_function = (fun i o -> if i=1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
-       classify_function = (fun o -> Substitute o)}
+       classify_function = classify_tactic_notation}
 
 let cons_production_parameter l = function
   | GramTerminal _ -> l
@@ -100,7 +104,7 @@ let rec next_key_away key t =
   if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
   else key
 
-let add_tactic_notation (n,prods,e) =
+let add_tactic_notation (local,n,prods,e) =
   let prods = List.map (interp_prod_item n) prods in
   let tags = make_tags prods in
   let key = next_key_away (tactic_notation_key prods) tags in
@@ -108,7 +112,7 @@ let add_tactic_notation (n,prods,e) =
   let ids = List.fold_left cons_production_parameter [] prods in
   let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
   let parule = (key,n,prods,(Lib.cwd(),tac)) in
-  Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule))
+  Lib.add_anonymous_leaf (inTacticGrammar (local,parule,pprule))
 
 (**********************************************************************)
 (* Printing grammar entries                                           *)
@@ -729,7 +733,7 @@ let classify_syntax_definition (local,_ as o) =
   if local then Dispose else Substitute o
 
 type syntax_extension_obj =
-    bool *
+    locality_flag *
       (notation_var_internalization_type list * Notation.level *
          notation * notation_grammar * unparsing list)
       list
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f95006e90..c7e1be39d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -19,7 +19,8 @@ val add_token_obj : string -> unit
 (** Adding a tactic notation in the environment *)
 
 val add_tactic_notation :
-  int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit
+  locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
+    unit
 
 (** Adding a (constr) notation in the environment*)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e629cf656..5c8efd3f8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1644,7 +1644,7 @@ let interp c = match c with
       assert false
 
   (* Syntax *)
-  | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
+  | VernacTacticNotation (b,n,r,e) -> Metasyntax.add_tactic_notation (b,n,r,e)
   | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl