Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tactiques

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

6 files changed, 37 insertions, 26 deletions

diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 33a6117da9..0c35b5cda3 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -15,7 +15,7 @@ open Pcoq
 open Genarg
 open Pp
 
-let pr_mlname _ _ s =
+let pr_mlname _ _ _ s =
   spc () ++
   (if !Options.v7 && not (Options.do_translate()) then qs s
   else Pptacticnew.qsnew s)
@@ -39,7 +39,7 @@ END
 
 (* Temporary for translator *)
 if !Options.v7 then
-  let pr_language _ _ = function
+  let pr_language _ _ _ = function
     | Ocaml -> str " Ocaml"
     | Haskell -> str " Haskell"
     | Scheme -> str " Scheme"
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 5d26686040..e29a91959e 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -115,7 +115,7 @@ END
 
 (* For the translator, otherwise the code above is OK *)
 open Ppconstrnew
-let pp_minus_div_arg _prc _prt (omin,odiv) = 
+let pp_minus_div_arg _prc _prlc _prt (omin,odiv) = 
   if omin=None && odiv=None then mt() else
     spc() ++ str "with" ++
     pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 29501d2a11..3f02cf309e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -44,16 +44,21 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) =
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) -> 
+    (constr_expr -> std_ppcmds) -> 
     (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    'a -> std_ppcmds
+
 type 'a glob_extra_genarg_printer =
     (rawconstr_and_expr -> std_ppcmds) ->
+    (rawconstr_and_expr -> std_ppcmds) ->
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    'a -> std_ppcmds
+
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) -> 
+    (Term.constr -> std_ppcmds) -> 
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    'a -> std_ppcmds
 
 let genarg_pprule_v7 = ref Stringmap.empty
 let genarg_pprule = ref Stringmap.empty
@@ -64,9 +69,9 @@ let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
     | _ -> error
 	"Can declare a pretty-printing rule only for extra argument types"
   in
-  let f prc prtac x = f prc prtac (out_gen rawwit x) in
-  let g prc prtac x = g prc prtac (out_gen globwit x) in
-  let h prc prtac x = h prc prtac (out_gen wit x) in
+  let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
+  let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
+  let h prc prlc prtac x = h prc prlc prtac (out_gen wit x) in
   genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7;
   if for_v8 then
     genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule 
@@ -296,7 +301,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
       let tab =
 	if Options.do_translate() or not !Options.v7 then !genarg_pprule
         else !genarg_pprule_v7 in
-      try pi1 (Stringmap.find s tab) prc prtac x
+      try pi1 (Stringmap.find s tab) prc prlc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
 
 
@@ -343,7 +348,7 @@ let rec pr_glob_generic prc prlc prtac x =
       let tab =
 	if Options.do_translate() or not !Options.v7 then !genarg_pprule
         else !genarg_pprule_v7 in
-      try pi2 (Stringmap.find s tab) prc prtac x
+      try pi2 (Stringmap.find s tab) prc prlc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
 
 open Closure
@@ -389,7 +394,7 @@ let rec pr_generic prc prlc prtac x =
       let tab = 
 	if Options.do_translate() or not !Options.v7 then !genarg_pprule
         else !genarg_pprule_v7 in
-      try pi3 (Stringmap.find s tab) prc prtac x
+      try pi3 (Stringmap.find s tab) prc prlc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "]"
 
 let rec pr_tacarg_using_rule pr_gen = function
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 3738c57bb9..9e1555ce91 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -23,16 +23,22 @@ val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
 val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    (constr_expr -> std_ppcmds) -> 
+    (constr_expr -> std_ppcmds) -> 
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
 
 type 'a glob_extra_genarg_printer =
-    (rawconstr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    (rawconstr_and_expr -> std_ppcmds) ->
+    (rawconstr_and_expr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
 
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    (Term.constr -> std_ppcmds) -> 
+    (Term.constr -> std_ppcmds) -> 
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
 
   (* if the boolean is false then the extension applies only to old syntax *)
 val declare_extra_genarg_pprule : 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index e3cb256325..e0cc336ca9 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -420,7 +420,7 @@ open Genarg
 
 (* Hint bases *)
 
-let pr_hintbases _prc _prt = function 
+let pr_hintbases _prc _prlc _prt = function 
   | None -> str " with *"
   | Some [] -> mt ()
   | Some l -> str " with " ++ Util.prlist_with_sep spc str l
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 3ac4c5d7dc..a31bc2cf04 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -22,7 +22,7 @@ open Tacinterp
 let _ = Metasyntax.add_token_obj "<-"
 let _ = Metasyntax.add_token_obj "->"
 
-let pr_orient _prc _prt = function
+let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
   | false -> Pp.str " <-"
 
@@ -34,7 +34,7 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 END
 
 (* For Setoid rewrite *)
-let pr_morphism_signature _ _ = Setoid_replace.pr_morphism_signature
+let pr_morphism_signature _ _ _ = Setoid_replace.pr_morphism_signature
 
 ARGUMENT EXTEND morphism_signature
  TYPED AS morphism_signature
@@ -48,9 +48,9 @@ ARGUMENT EXTEND morphism_signature
        [ let l,out = s in (None,c)::l,out ]
 END
 
-let pr_gen prc _ c = prc c
+let pr_gen prc _prlc _prtac c = prc c
 
-let pr_rawc _ _ raw = Ppconstr.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac raw = Ppconstr.pr_rawconstr raw
 
 let interp_raw _ _ (t,_) = t
 
@@ -87,8 +87,8 @@ let pr_gen_place pr_id = function
   | HypLocation (id,InHypValueOnly) -> 
       str "in (Value of " ++ pr_id id ++ str ")"
 
-let pr_loc_place _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id)
-let pr_place _ _ = pr_gen_place Nameops.pr_id
+let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id)
+let pr_place _ _ _ = pr_gen_place Nameops.pr_id
 
 let intern_place ist = function
     ConclLocation () -> ConclLocation ()