- 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

1 files changed, 8 insertions, 5 deletions

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