- 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

8 files changed, 43 insertions, 32 deletions

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 >>