1 files changed, 0 insertions, 88 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index c156e869d..dc41cf8e3 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -208,94 +208,6 @@ END
 
 let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
 
-let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds =
-  match lo,concl with
-    | Some [],true -> mt ()
-    | None,true -> str "in" ++ spc () ++ str "*"
-    | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
-    | Some l,_ ->
-	str "in" ++
-         spc () ++ prlist_with_sep pr_comma pr_id l ++
-	  match concl with
-	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
-	    | _ -> mt ()
-
-
-let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id)
-
-let pr_in_arg_hyp_typed  _ _  _  = pr_in_hyp Ppconstr.pr_id
-
-
-let pr_var_list_gen pr_id = Pp.prlist_with_sep (fun () -> str ",") pr_id
-
-let pr_var_list_typed _ _ _ =  pr_var_list_gen Ppconstr.pr_id
-
-let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id)
-
-
-ARGUMENT EXTEND comma_var_lne
-  PRINTED BY pr_var_list_typed
-  RAW_TYPED AS var list
-  RAW_PRINTED BY pr_var_list
-  GLOB_TYPED AS var list
-  GLOB_PRINTED BY pr_var_list
-| [ var(x) ] -> [ [x] ]
-| [ var(x) "," comma_var_lne(l) ] -> [x::l]
-END
-
-ARGUMENT EXTEND comma_var_l
-  PRINTED BY pr_var_list_typed
-  RAW_TYPED AS var list
-  RAW_PRINTED BY pr_var_list
-  GLOB_TYPED AS var list
-  GLOB_PRINTED BY pr_var_list
-| [  comma_var_lne(l) ] -> [l]
-| [] -> [ [] ]
-END
-
-let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-"
-
-ARGUMENT EXTEND inconcl
-  TYPED AS bool
-  PRINTED BY pr_in_concl
-| [ "|-" "*" ] -> [ true ]
-| [ "|-" ] -> [ false ]
-END
-
-
-
-ARGUMENT EXTEND in_arg_hyp
-  PRINTED BY pr_in_arg_hyp_typed
-  RAW_TYPED AS var list option * bool
-  RAW_PRINTED BY pr_in_arg_hyp
-  GLOB_TYPED AS var list option * bool
-  GLOB_PRINTED BY pr_in_arg_hyp
-| [ "in" "*" ] -> [(None,true)]
-| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)]
-| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in
-					      Some l, onconcl
-					   ]
-| [ ] -> [ (Some [],true) ]
-END
-
-let pr_in_arg_hyp = pr_in_arg_hyp_typed () () ()
-
-let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : clause =
-  {onhyps=
-   Option.map
-     (fun l ->
-	List.map
-	  (fun id -> ( (AllOccurrences,trad_id id),InHyp))
-	  l
-     )
-     hyps;
-   concl_occs = if concl then AllOccurrences else NoOccurrences}
-
-
-let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd
-let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
-
-
 (* spiwack argument for the commands of the retroknowledge *)
 
 let wit_r_nat_field =