- Export de pattern_ident vers les ARGUMENT EXTEND and co.

- Extension du test de réversibilité acyclique des notations dures aux
  notations de type abbréviation (du genre inhabited A := A).
- Ajout options Local/Global à Transparent/Opaque.
- Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé 
  dependent retiré).



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

22 files changed, 130 insertions, 93 deletions

diff --git a/CHANGES b/CHANGES
index 6550be7059..7b233e2a07 100644
--- a/CHANGES
+++ b/CHANGES
@@ -62,6 +62,7 @@ Vernacular commands
   conversion tests. It generalizes commands Opaque and Transparent by
   introducing a range of levels. Lower levels are assigned to constants
   that should be expanded first.
+- New options Global and Local to Opaque and Transparent.
 - New command "Print Assumptions" to display all variables, parameters
   or axioms a theorem or definition relies on.
 - "Add Rec LoadPath" now provides references to libraries using partially
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a2285015dc..d7d2f6d8ea 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -340,7 +340,8 @@ let rec pr_argument_type = function
   | StringArgType -> str"string"
   | PreIdentArgType -> str"pre-ident"
   | IntroPatternArgType -> str"intro-pattern"
-  | IdentArgType -> str"ident"
+  | IdentArgType true -> str"ident"
+  | IdentArgType false -> str"pattern_ident"
   | VarArgType -> str"var"
   | RefArgType -> str"ref"
   (* Specific types *)
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 7c6bf7297c..8bcffb4ff6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -886,19 +886,24 @@ computation of algebraic values, such as numbers, and for reflexion-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.
 
-\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold
+\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} 
+This command has an effect on unfoldable constants, i.e. 
+on constants defined by {\tt Definition} or {\tt Let} (with an explicit
+body), or by a command assimilated to a definition such as {\tt
+Fixpoint}, {\tt Program Definition}, etc, or by a proof ended by {\tt
+Defined}. The command tells not to unfold
 the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
-$\delta$-conversion. Unfolding a constant is replacing it by its
-definition. {\tt Opaque} can only apply on constants originally
-defined as {\tt Transparent}.
-
-Constants defined by a proof ended by {\tt Qed} are automatically
-stamped as {\tt Opaque} and can no longer be considered as {\tt
-Transparent}. This is to keep with the usual mathematical practice of
-{\em proof irrelevance}: what matters in a mathematical development is
-the sequence of lemma statements, not their actual proofs. This
-distinguishes lemmas from the usual defined constants, whose actual
-values are of course relevant in general.
+$\delta$-conversion (unfolding a constant is replacing it by its
+definition).
+
+{\tt Opaque} has also on effect on the conversion algorithm of {\Coq},
+telling to delay the unfolding of a constant as later as possible in
+case {\Coq} has to check the conversion (see Section~\ref{conv-rules})
+of two distinct applied constants.
+
+The scope of {\tt Opaque} is limited to the current section, or
+current file, unless the variant {\tt Opaque Global \qualid$_1$ \dots
+\qualid$_n$} is used.
 
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
 \ref{Theorem}
@@ -912,19 +917,21 @@ environment}\\
 \end{ErrMsgs}
 
 \subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}}
-This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behavior after an {\tt Opaque} command.
-
-The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
-  Definition} or {\tt Local} with an explicit body.
-
-\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
-with the reset mechanism. If a constant was transparent at point A, if
-you set it opaque at point B and reset to point A, you return to state
-of point A with the difference that the constant is still opaque. This
-can cause changes in tactic scripts behavior.
+This command is the converse of {\tt Opaque} and it applies on
+unfoldable constants to restore their unfoldability after an {\tt
+Opaque} command.
+
+Note in particular that constants defined by a proof ended by {\tt
+Qed} are not unfoldable and {\tt Transparent} has no effect on
+them. This is to keep with the usual mathematical practice of {\em
+proof irrelevance}: what matters in a mathematical development is the
+sequence of lemma statements, not their actual proofs. This
+distinguishes lemmas from the usual defined constants, whose actual
+values are of course relevant in general.
 
-At section or module closing, a constant recovers the status it got at
-the time of its definition.
+The scope of {\tt Transparent} is limited to the current section, or
+current file, unless the variant {\tt Transparent Global \qualid$_1$
+\dots \qualid$_n$} is used.
 
 \begin{ErrMsgs}
 % \item \errindex{Can not set transparent.}\\
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ca06e1d782..00e8a3ecef 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -202,16 +202,6 @@ This moves {\ident} at the top of the local context (at the beginning of the con
 
 This moves {\ident} at the bottom of the local context (at the end of the context).
 
-\item {\tt move dependent {\ident$_1$} after {\ident$_2$}}\\
-      {\tt move dependent {\ident$_1$} before {\ident$_2$}}\\
-      {\tt move dependent {\ident$_1$} at top}\\
-      {\tt move dependent {\ident$_1$} at bottom}
-
-This moves {\ident$_1$} towards the specified place. All the
-hypotheses that recursively depend on, for a downwards move, or
-in, for an upwards move, the hypothesis {\ident$_1$} are moved
-too so as to respect the order of dependencies between hypotheses.
-
 \end{Variants}
 
 \begin{ErrMsgs}
diff --git a/interp/genarg.ml b/interp/genarg.ml
index d1eda47b78..35107c8080 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -26,7 +26,7 @@ type argument_type =
   | StringArgType
   | PreIdentArgType
   | IntroPatternArgType
-  | IdentArgType
+  | IdentArgType of bool
   | VarArgType
   | RefArgType
   (* Specific types *)
@@ -126,9 +126,17 @@ let rawwit_intro_pattern = IntroPatternArgType
 let globwit_intro_pattern = IntroPatternArgType
 let wit_intro_pattern = IntroPatternArgType
 
-let rawwit_ident = IdentArgType
-let globwit_ident = IdentArgType
-let wit_ident = IdentArgType
+let rawwit_ident_gen b = IdentArgType b
+let globwit_ident_gen b = IdentArgType b
+let wit_ident_gen b = IdentArgType b
+
+let rawwit_ident = rawwit_ident_gen true
+let globwit_ident = globwit_ident_gen true
+let wit_ident = wit_ident_gen true
+
+let rawwit_pattern_ident = rawwit_ident_gen false
+let globwit_pattern_ident = globwit_ident_gen false
+let wit_pattern_ident = wit_ident_gen false
 
 let rawwit_var = VarArgType
 let globwit_var = VarArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 0ced1e5bea..92c7db36f4 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -86,7 +86,8 @@ IntArgType                     int                       int
 IntOrVarArgType                int or_var                int
 StringArgType                  string (parsed w/ "")     string
 PreIdentArgType                string (parsed w/o "")    (vernac only)
-IdentArgType                   identifier                identifier
+IdentArgType true              identifier                identifier
+IdentArgType false             identifier (pattern_ident) identifier
 IntroPatternArgType            intro_pattern_expr        intro_pattern_expr
 VarArgType                     identifier located        identifier
 RefArgType                     reference                 global_reference
@@ -145,6 +146,14 @@ val rawwit_ident : (identifier,rlevel) abstract_argument_type
 val globwit_ident : (identifier,glevel) abstract_argument_type
 val wit_ident : (identifier,tlevel) abstract_argument_type
 
+val rawwit_pattern_ident : (identifier,rlevel) abstract_argument_type
+val globwit_pattern_ident : (identifier,glevel) abstract_argument_type
+val wit_pattern_ident : (identifier,tlevel) abstract_argument_type
+
+val rawwit_ident_gen : bool -> (identifier,rlevel) abstract_argument_type
+val globwit_ident_gen : bool -> (identifier,glevel) abstract_argument_type
+val wit_ident_gen : bool -> (identifier,tlevel) abstract_argument_type
+
 val rawwit_var : (identifier located,rlevel) abstract_argument_type
 val globwit_var : (identifier located,glevel) abstract_argument_type
 val wit_var : (identifier,tlevel) abstract_argument_type
@@ -257,7 +266,7 @@ type argument_type =
   | StringArgType
   | PreIdentArgType
   | IntroPatternArgType
-  | IdentArgType
+  | IdentArgType of bool
   | VarArgType
   | RefArgType
   (* Specific types *)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index b4fa39bebe..770a54a78e 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -25,7 +25,7 @@ let rec make_rawwit loc = function
   | StringArgType -> <:expr< Genarg.rawwit_string >>
   | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
   | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
-  | IdentArgType -> <:expr< Genarg.rawwit_ident >>
+  | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >>
   | VarArgType -> <:expr< Genarg.rawwit_var >>
   | RefArgType -> <:expr< Genarg.rawwit_ref >>
   | SortArgType -> <:expr< Genarg.rawwit_sort >>
@@ -50,7 +50,7 @@ let rec make_globwit loc = function
   | StringArgType -> <:expr< Genarg.globwit_string >>
   | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
   | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
-  | IdentArgType -> <:expr< Genarg.globwit_ident >>
+  | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >>
   | VarArgType -> <:expr< Genarg.globwit_var >>
   | RefArgType -> <:expr< Genarg.globwit_ref >>
   | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
@@ -75,7 +75,7 @@ let rec make_wit loc = function
   | StringArgType -> <:expr< Genarg.wit_string >>
   | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
   | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
-  | IdentArgType -> <:expr< Genarg.wit_ident >>
+  | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >>
   | VarArgType -> <:expr< Genarg.wit_var >>
   | RefArgType -> <:expr< Genarg.wit_ref >>
   | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e62fb70768..ec84c6ed81 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -588,8 +588,8 @@ GEXTEND Gram
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
       | IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
       | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
-      | IDENT "move"; dep = [IDENT "dependent" -> true | -> false]; 
-	  hfrom = id_or_meta; hto = move_location -> TacMove (dep,hfrom,hto)
+      | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
+	  TacMove (true,hfrom,hto)
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
       | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 76ec0c0901..b22ae3fedd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -105,6 +105,15 @@ GEXTEND Gram
   ;
 END
 
+GEXTEND Gram
+  GLOBAL: locality non_locality;
+  locality:
+    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ]
+  ;
+  non_locality:
+    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
+  ;
+END
 
 let test_plurial_form = function
   | [(_,([_],_))] ->
@@ -440,10 +449,10 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
-        IDENT "Transparent"; l = LIST1 global ->
-          VernacSetOpacity (true,[Conv_oracle.transparent,l])
-      | IDENT "Opaque"; l = LIST1 global ->
-          VernacSetOpacity (true,[Conv_oracle.Opaque, l])
+        IDENT "Transparent"; b = non_locality; l = LIST1 global ->
+          VernacSetOpacity (b,[Conv_oracle.transparent,l])
+      | IDENT "Opaque"; b = non_locality; l = LIST1 global ->
+          VernacSetOpacity (b,[Conv_oracle.Opaque, l])
       | IDENT "Strategy"; l =
           LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
             VernacSetOpacity (false,l)
@@ -788,7 +797,7 @@ GEXTEND Gram
 ;;
 
 (* Grammar extensions *)
-	  
+
 GEXTEND Gram
   GLOBAL: syntax;
 
@@ -805,7 +814,7 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; 
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; local = non_globality; qid = global;
+     | IDENT "Arguments"; IDENT "Scope"; local = non_locality; qid = global;
        "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl)
 
      | IDENT "Infix"; local = locality;
@@ -837,12 +846,6 @@ GEXTEND Gram
   tactic_level:
     [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
   ;
-  locality:
-    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ]
-  ;
-  non_globality:
-    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
-  ;
   level:
     [ [ IDENT "level"; n = natural -> NumLevel n
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cee08f2341..69c1164f1f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -407,7 +407,7 @@ module Prim =
 
     let name = Gram.Entry.create "Prim.name"
     let identref = Gram.Entry.create "Prim.identref"
-    let pattern_ident = Gram.Entry.create "pattern_ident"
+    let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident"
     let pattern_identref = Gram.Entry.create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
@@ -495,6 +495,9 @@ module Vernac_ =
   struct
     let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
 
+    let locality = gec_vernac "locality"
+    let non_locality = gec_vernac "non_locality"
+
     (* The different kinds of vernacular commands *)
     let gallina = gec_vernac "gallina"
     let gallina_ext = gec_vernac "gallina_ext"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 824ca640e8..d1c062e117 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -199,6 +199,8 @@ module Tactic :
 module Vernac_ :
   sig
     open Decl_kinds
+    val locality : bool Gram.Entry.e
+    val non_locality : bool Gram.Entry.e
     val gallina : vernac_expr Gram.Entry.e
     val gallina_ext : vernac_expr Gram.Entry.e
     val command : vernac_expr Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d2ba5ffbc6..b37cb9fce4 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -140,6 +140,8 @@ let out_bindings = function
   | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l)
   | NoBindings -> NoBindings
 
+let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
+
 let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
@@ -148,7 +150,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
   | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
   | PreIdentArgType -> str (out_gen rawwit_pre_ident x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
-  | IdentArgType -> pr_id (out_gen rawwit_ident x)
+  | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x)
   | VarArgType -> pr_located pr_id (out_gen rawwit_var x)
   | RefArgType -> prref (out_gen rawwit_ref x)
   | SortArgType -> pr_rawsort (out_gen rawwit_sort x)
@@ -190,7 +192,7 @@ let rec pr_glob_generic prc prlc prtac x =
   | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
   | PreIdentArgType -> str (out_gen globwit_pre_ident x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
-  | IdentArgType -> pr_id (out_gen globwit_ident x)
+  | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x)
   | VarArgType -> pr_located pr_id (out_gen globwit_var x)
   | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
   | SortArgType -> pr_rawsort (out_gen globwit_sort x)
@@ -236,7 +238,7 @@ let rec pr_generic prc prlc prtac x =
   | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
   | PreIdentArgType -> str (out_gen wit_pre_ident x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
-  | IdentArgType -> pr_id (out_gen wit_ident x)
+  | IdentArgType b -> if_pattern_ident b pr_id (out_gen wit_ident x)
   | VarArgType -> pr_id (out_gen wit_var x)
   | RefArgType -> pr_global (out_gen wit_ref x)
   | SortArgType -> pr_sort (out_gen wit_sort x)
@@ -805,9 +807,10 @@ and pr_atom1 = function
   | TacClearBody l ->
       hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->
+      (* Rem: only b = true is available for users *)
+      assert b;
       hov 1
-        (str "move" ++ (if b then spc () ++ str"dependent" else mt ())
-	  ++ brk (1,1) ++ pr_ident id1 ++ 
+        (str "move" ++ brk (1,1) ++ pr_ident id1 ++ 
 	 pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6cfd277a0e..f779f53fb7 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -146,7 +146,7 @@ let pr_search a b pr_p = match a with
   | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
 
 let pr_locality local = if local then str "Local " else str ""
-let pr_non_globality local = if local then str "" else str "Global "
+let pr_non_locality local = if local then str "" else str "Global "
 
 let pr_explanation (e,b,f) =
   let a = match e with
@@ -486,7 +486,7 @@ let rec pr_vernac = function
   | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function 
       |	None -> str"_"
       |	Some sc -> str sc in 
-    str"Arguments Scope" ++ spc() ++ pr_non_globality local ++ pr_reference q 
+    str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ pr_reference q 
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
@@ -708,7 +708,7 @@ let rec pr_vernac = function
 	
  | VernacInstance (glob, sup, (instid, bk, cl), props, pri) -> 
      hov 1 (
-       pr_non_globality (not glob) ++
+       pr_non_locality (not glob) ++
        str"Instance" ++ spc () ++ 
 	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++ 
@@ -824,7 +824,7 @@ let rec pr_vernac = function
   | VernacDeclareImplicits (local,q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
   | VernacDeclareImplicits (local,q,Some imps) ->
-      hov 1 (str"Implicit Arguments " ++ pr_non_globality local ++
+      hov 1 (str"Implicit Arguments " ++ pr_non_locality local ++
 	spc() ++ pr_reference q ++ spc() ++
 	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
   | VernacReserve (idl,c) ->
@@ -832,11 +832,11 @@ let rec pr_vernac = function
         str (if List.length idl > 1 then "s " else " ") ++
         prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++
         pr_lconstr c)
-  | VernacSetOpacity(true,[k,l]) when k=Conv_oracle.transparent ->
-      hov 1 (str"Transparent" ++
+  | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
+      hov 1 (str"Transparent" ++ pr_non_locality b ++
              spc() ++ prlist_with_sep sep pr_reference l)
-  | VernacSetOpacity(true,[Conv_oracle.Opaque,l]) ->
-      hov 1 (str"Opaque" ++
+  | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
+      hov 1 (str"Opaque" ++ pr_non_locality b ++
              spc() ++ prlist_with_sep sep pr_reference l)
   | VernacSetOpacity (local,l) ->
       let pr_lev = function
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 31054c7f52..37350af08b 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -197,7 +197,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
   | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
   | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
-  | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
+  | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 71e7cdc21e..c7d6ffe14f 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -46,12 +46,13 @@ let set_strategy_one ref l  =
         Csymtable.set_transparent_const sp
     | _ -> ()
 
-let cache_strategy str =
+let cache_strategy (_,str) =
   List.iter 
     (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
     str
 
-let subst_strategy (_,subs,obj) =
+let subst_strategy (_,subs,(local,obj)) =
+  local,
   list_smartmap
     (fun (k,ql as entry) ->
       let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
@@ -68,14 +69,16 @@ let map_strategy f l =
               Some q' -> q' :: ql
             | None -> ql) ql [] in
       if ql'=[] then str else (lev,ql')::str) l [] in
-  if l'=[] then None else Some l'
+  if l'=[] then None else Some (false,l')
 
-let export_strategy obj =
+let export_strategy (local,obj) =
+  if local then None else
   map_strategy (function
       EvalVarRef _ -> None
     | EvalConstRef _ as q -> Some q) obj
 
-let classify_strategy (_,obj) = Substitute obj
+let classify_strategy (_,(local,_ as obj)) = 
+  if local then Dispose else Substitute obj
 
 let disch_ref ref =
   match ref with
@@ -84,7 +87,8 @@ let disch_ref ref =
         if c==c' then Some ref else Some (EvalConstRef c')
     | _ -> Some ref
 
-let discharge_strategy (_,obj) =
+let discharge_strategy (_,(local,obj)) =
+  if local then None else
   map_strategy disch_ref obj
 
 let (inStrategy,outStrategy) =
@@ -98,8 +102,7 @@ let (inStrategy,outStrategy) =
 
 
 let set_strategy local str =
-  if local then cache_strategy str
-  else Lib.add_anonymous_leaf (inStrategy str)
+  Lib.add_anonymous_leaf (inStrategy (local,str))
 
 let _ = 
   Summary.declare_summary "Transparent constants and variables"
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 72500c7e3d..e2456adc1d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -937,9 +937,10 @@ and intern_genarg ist x =
       (* how to know which names are bound by the intropattern *)
       in_gen globwit_intro_pattern
         (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
-  | IdentArgType ->
+  | IdentArgType b ->
       let lf = ref ([],[]) in
-      in_gen globwit_ident(intern_ident lf ist (out_gen rawwit_ident x))
+      in_gen (globwit_ident_gen b) 
+	(intern_ident lf ist (out_gen (rawwit_ident_gen b) x))
   | VarArgType ->
       in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
   | RefArgType ->
@@ -1994,9 +1995,9 @@ and interp_genarg ist gl x =
   | IntroPatternArgType ->
       in_gen wit_intro_pattern
         (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
-  | IdentArgType ->
-      in_gen wit_ident
-        (interp_fresh_ident ist gl (out_gen globwit_ident x))
+  | IdentArgType b ->
+      in_gen (wit_ident_gen b)
+        (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))
   | VarArgType ->
       in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x))
   | RefArgType ->
@@ -2325,10 +2326,10 @@ and interp_atomic ist gl = function
     | IntroPatternArgType ->
 	VIntroPattern 
 	  (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)))
-    | IdentArgType -> 
+    | IdentArgType b ->
         VIntroPattern 
 	  (IntroIdentifier
-              (interp_fresh_ident ist gl (out_gen globwit_ident x)))
+              (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)))
     | VarArgType ->
         mk_hyp_value ist gl (out_gen globwit_var x)
     | RefArgType -> 
@@ -2676,7 +2677,8 @@ and subst_genarg subst (x:glob_generic_argument) =
   | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
   | IntroPatternArgType ->
       in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
-  | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x)
+  | IdentArgType b -> 
+      in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x)
   | VarArgType -> in_gen globwit_var (out_gen globwit_var x)
   | RefArgType ->
       in_gen globwit_ref (subst_global_reference subst 
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 8555886023..dad60fb779 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -21,7 +21,7 @@ Set Implicit Arguments.
 Require Export Classical.
 Require Import ChoiceFacts.
 
-Notation Local inhabited A := A.
+Notation Local inhabited A := A (only parsing).
 
 Axiom constructive_definite_description :
   forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 6673fa8c96..d4ba4a3a7b 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -119,7 +119,7 @@ Qed.
 
 *)
 
-Notation Local inhabited A := A.
+Notation Local inhabited A := A (only parsing).
 
 Lemma prop_ext_A_eq_A_imp_A :
   prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index b96ae30e4e..95a07f2f3c 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
 
 (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
 
-Notation Local inhabited A := A.
+Notation Local inhabited A := A (only parsing).
 
 Section ExtensionalEpsilon_imp_EM.
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c8acd81135..ca55fb0663 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -167,6 +167,7 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
 
 let syntax_definition ident (vars,c) local onlyparse =
   let pat = interp_aconstr [] vars c in
+  let onlyparse = onlyparse or Metasyntax.is_not_printable (snd pat) in
   Syntax_def.declare_syntactic_definition local ident onlyparse pat
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a14d42074d..b43a5eeb9f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -745,7 +745,7 @@ let check_rule_productivity l =
     error "A recursive notation must start with at least one symbol."
 
 let is_not_printable = function
-  | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
+  | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
   | _ -> false
 
 let find_precedence lev etyps symbols =
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 1f6b914726..d4b61eb003 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -56,3 +56,7 @@ val print_grammar : string -> unit
 (* Removes quotes in a notation *)
 
 val standardize_locatable_notation : string -> string
+
+(* Evaluate whether a notation is not printable *)
+
+val is_not_printable : aconstr -> bool