Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; pf_get_new_id moved to Tacmach)

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

2 files changed, 0 insertions, 83 deletions

diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index f5723fe368..fd0a8f9d2a 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -29,74 +29,3 @@ open Evar_refiner
    write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
    -- Eduardo (11/8/97) *)
 
-let pf_get_new_id id gls = 
-  next_ident_away id (pf_ids_of_hyps gls)
-
-let pf_get_new_ids ids gls =
-  let avoid = pf_ids_of_hyps gls in
-  List.fold_right
-    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
-    ids []
-
-(* What follows is part of the contents of the former file tactics3.ml *)
-(* 2/2002: replaced THEN_i by THENSLAST to solve a bug in
-   Tacticals.general_elim when the eliminator has missing bindings *)
-
-let rec build_args acc ce p_0 p_1 =
-  match kind_of_term p_0, p_1 with 
-    | (Prod (na,a,b), (a_0::bargs)) ->
-        let (newa,ce') = (build_term ce (na,Some a) a_0) in 
-	build_args (newa::acc) ce' (subst1 a_0 b) bargs
-    | (LetIn (na,a,t,b), args) -> build_args acc ce (subst1 a b) args
-    | (_, [])     -> (List.rev acc,ce)
-    | (_, (_::_)) -> failwith "mk_clenv_using"
-
-and build_term ce p_0 c =
-  let env = w_env ce.hook in
-  match p_0, kind_of_term c with 
-    | ((na,Some t), Meta mv) -> 
-(*    	let mv = new_meta() in *)
-	(mkMeta mv, clenv_pose (na,mv,t) ce)
-    | ((na,_), Cast (c,t)) -> build_term ce (na,Some t) c
-    | ((na,Some t), _) ->
-    	if (not((occur_meta c))) then 
-	  (c,ce)
-    	else 
-	  let (hd,args) = 
-	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c in
-          let hdty = w_type_of ce.hook hd in
-          let (args,ce') =
-	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
-          let newc = applist(hd,args) in
-          let t' = clenv_type_of ce' newc in  
-	  if w_conv_x ce'.hook t t' then 
-	    (newc,ce') 
-	  else 
-	    failwith "mk_clenv_using"
-    | ((na,None), _) ->
-    	if (not((occur_meta c))) then 
-	  (c,ce)
-    	else 
-	  let (hd,args) = 
-	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c in
-          let hdty = w_type_of ce.hook hd in
-          let (args,ce') = 
-	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
-          let newc = applist(hd,args) in
-	  (newc,ce')
-
-let mk_clenv_using wc c =
-  let ce = mk_clenv wc mkProp in
-  let (newc,ce') = 
-    try 
-      build_term ce (Anonymous,None) c
-    with Failure _ -> 
-      raise (RefinerError (NotWellTyped c))
-  in
-  clenv_change_head (newc,clenv_type_of ce' newc) ce'
-
-let applyUsing c gl =
-  let (wc,kONT) = startWalk gl in
-  let clause = mk_clenv_using wc c in 
-  res_pf kONT clause gl
-
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 7493e813c7..4951df54bb 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -22,15 +22,3 @@ open Clenv
 
 (* A somewhat cryptic module. *)
 
-val pf_get_new_id  : identifier      -> goal sigma -> identifier
-val pf_get_new_ids : identifier list -> goal sigma -> identifier list
-
-(*i**
-val add_prod_sign : 
-  'a evar_map -> constr * types signature -> constr * types signature
-
-val add_prods_sign : 
-  'a evar_map -> constr * types signature -> constr * types signature
-**i*)
-
-val applyUsing : constr -> tactic