1 files changed, 1 insertions, 59 deletions
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 01ae688ad5..c5c7319e8d 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -19,7 +19,6 @@ open Reductionops
 open Declarations
 open Formula
 open Sequent
-open Unify
 open Libnames
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
@@ -193,64 +192,7 @@ let ll_forall_tac prod id tacrec seq=
 
 (* complicated stuff for instantiation with unification *)
 
-let rec collect_forall seq=
-  if is_empty_left seq then ([],seq) 
-  else
-    let hd,seq1=take_left seq in
-      (match hd.pat with 
-	   Lforall(_,_,_)-> 
-	     let (q,seq2)=collect_forall seq1 in
-	       ((hd::q),seq2)
-	 | _->[],seq)
-
-let left_instance_tac (inst,id) tacrec seq=
-  match inst with
-      Phantom dom->
-	if lookup id None seq then 
-	  tclFAIL 0 "already done"
-	else
-	  tclTHENS (cut dom) 
-	    [tclTHENLIST
-	       [intro;
-		(fun gls->generalize 
-		   [mkApp(constr_of_reference id,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		intro;
-		tclSOLVE [wrap 1 false tacrec 
-			    (deepen (record id None seq))]];
-	    tclTRY assumption]
-    | Real(t,_)->
-	if lookup id (Some t) seq then 
-	  tclFAIL 0 "already done" 
-	else
-	  tclTHENLIST 
-	    [generalize [mkApp(constr_of_reference id,[|t|])];
-	     intro; 
-	     tclSOLVE 
-	       [wrap 1 false tacrec 
-		  (deepen (record id (Some t) seq))]]
-
-let left_forall_tac lfp tacrec seq gl=
-  let insts=give_left_instances lfp seq in
-    tclFIRST (List.map (fun inst->left_instance_tac inst tacrec seq) insts) gl
-	  
-let dummy_exists_tac dom  tacrec seq=
-	tclTHENS (cut dom) 
-	[tclTHENLIST
-	   [intro;
-	    (fun gls->
-	       split (Rawterm.ImplicitBindings 
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
-	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
-	 tclTRY assumption] 
- 
-let right_instance_tac (t,_) tacrec seq=
-	tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	(tclSOLVE [wrap 0 true tacrec (deepen seq)])
-
-let exists_tac insts tacrec seq gl=
-    tclFIRST 
-      (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl
+(* moved to instances.ml *)
 
 (* special for compatibility with old Intuition *)