1 files changed, 5 insertions, 66 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index fd732563a..37b8b3356 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -19,88 +19,27 @@ open Genarg
 let _ = Metasyntax.add_token_obj "<-"
 let _ = Metasyntax.add_token_obj "->"
 
-let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-"
+let pr_orient _prc _prt = function true -> Pp.str " ->" | false -> Pp.str " <-"
 
 ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ "->" ] -> [ true ]
 | [ "<-" ] -> [ false ]
 | [ ] -> [ true ]
 END
-(*
-let wit_orient, rawwit_orient = Genarg.create_arg "orient"
-let orient = Pcoq.create_generic_entry "orient" rawwit_orient
-let _ = Tacinterp.add_genarg_interp "orient"
-  (fun ist x ->
-    (in_gen wit_orient
-      (out_gen wit_bool
-	(Tacinterp.genarg_interp ist
-	  (in_gen wit_bool
-	    (out_gen rawwit_orient x))))))
-
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
-
-GEXTEND Gram
-  GLOBAL: orient;
-  orient:
-  [ [ "->" -> true
-    | "<-" -> false
-    | -> true ] ];
-END
-
-let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-"
-
-let _ = 
-  Pptactic.declare_extra_genarg_pprule
-    (rawwit_orient, pr_orient)
-    (wit_orient, pr_orient)
-*)
  
 (* with_constr *)
 
 open Tacinterp
 
-let pr_with_constr_gen prc = function 
+let pr_with_constr_gen prc _prtac = function 
   | None -> Pp.mt ()
   | Some c -> Pp.str " with" ++ prc c
 
-let rawpr_with_constr = pr_with_constr_gen Ppconstr.pr_constr
-let pr_with_constr = pr_with_constr_gen Printer.prterm
-
 ARGUMENT EXTEND with_constr
   TYPED AS constr_opt 
-  PRINTED BY pr_with_constr 
-  INTERPRETED BY genarg_interp
-  RAW TYPED AS constr_opt
-  RAW PRINTED BY rawpr_with_constr
+  PRINTED BY pr_with_constr_gen 
+  INTERPRETED BY interp_genarg
+  GLOBALIZED BY intern_genarg
 | [ "with" constr(c) ] -> [ Some c ]
 | [ ] -> [ None ]
 END
-
-(*
-let wit_with_constr, rawwit_with_constr = Genarg.create_arg "with_constr"
-let with_constr = Pcoq.create_generic_entry "with_constr" rawwit_with_constr
-let _ = Tacinterp.add_genarg_interp "with_constr"
-  (fun ist x ->
-    (in_gen wit_with_constr
-      (out_gen (wit_opt wit_constr)
-	(Tacinterp.genarg_interp ist
-	  (in_gen (wit_opt rawwit_constr)
-	    (out_gen rawwit_with_constr x))))))
-
-GEXTEND Gram
-  GLOBAL: with_constr;
-  with_constr:
-  [ [ "with"; c = Constr.constr -> Some c
-    | -> None ] ];
-END
-
-let pr_with_constr prc = function 
-  | None -> Pp.mt ()
-  | Some c -> Pp.str " with" ++ prc c
-
-let _ = 
-  Pptactic.declare_extra_genarg_pprule
-    (rawwit_with_constr, pr_with_constr Ppconstr.pr_constr)
-    (wit_with_constr, pr_with_constr Printer.prterm)
-*)