Major Ground tactic update, sensible performance improvement

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

9 files changed, 331 insertions, 133 deletions

diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4
index 07864fe9bf..612ac309b7 100644
--- a/contrib/first-order/engine.ml4
+++ b/contrib/first-order/engine.ml4
@@ -56,12 +56,16 @@ let ground_tac solver startseq gl=
 	    (or_tac toptac (re_add seq))
 	    (left_tac seq ctx) gl
 	| Rexists(i,dom)->
-	    tclORELSE
-	    (if seq.depth<=0 || not !qflag then 
-	       tclFAIL 0 "max depth" 
-	     else 
-	       exists_tac i dom atoms toptac (re_add seq))
-	    (left_tac seq ctx) gl
+	    let cont_tac=left_tac seq ctx in
+	      if seq.depth<=0 || not !qflag then 
+		cont_tac gl
+	      else 
+		(match Unify.give_right_instances i dom atoms seq with
+		    Some l -> tclORELSE
+		      (exists_tac l toptac (re_add seq)) cont_tac gl
+		  | None ->
+		      tclORELSE cont_tac
+		      (dummy_exists_tac dom  toptac (re_add seq)) gl)
 	| _-> anomaly "unreachable place"
   and left_tac seq ctx gl=
     if is_empty_left seq then 
@@ -77,13 +81,13 @@ let ground_tac solver startseq gl=
 	  | Lor ind->
 	      left_or_tac ind hd.id toptac (re_add seq1) gl
 	  | Lforall (i,dom)->
-	      tclORELSE
-	      (if seq.depth<=0 || not !qflag then 
-		 tclFAIL 0 "max depth" 
-	       else 
-		 left_forall_tac i dom hd.atoms hd.internal hd.id
-		    toptac (re_add seq))
-	      (left_tac seq1 (hd::ctx)) gl
+	      let (lfp,seq2)=collect_forall seq in
+		tclORELSE
+		  (if seq.depth<=0 || not !qflag then 
+		     tclFAIL 0 "max depth" 
+		   else 
+		     left_forall_tac lfp toptac (re_add seq))
+		  (left_tac seq2 (lfp@ctx)) gl
 	  | Lexists ->
 	      if !qflag then
 		left_exists_tac hd.id toptac (re_add seq1) gl
@@ -130,18 +134,23 @@ let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
 let fail_solver=tclFAIL 0 "GroundTauto failed"
 		      
 let gen_ground_tac flag taco io l=
-  qflag:=flag;
-  let depth=
-    match io with 
-	Some i->i
-      | None-> !Auto.default_search_depth in
-  let solver= 
-    match taco with 
-	Some tac->tac
-      | None-> default_solver in
-  let startseq=create_with_ref_list l depth in
-    ground_tac solver startseq
-
+  let backup= !qflag in
+    try
+      qflag:=flag;
+      let depth=
+	match io with 
+	    Some i->i
+	  | None-> !Auto.default_search_depth in
+      let solver= 
+	match taco with 
+	    Some tac->tac
+	  | None-> default_solver in
+      let startseq=create_with_ref_list l depth in
+      let result=
+	ground_tac solver startseq
+      in qflag:=backup;result
+    with e -> qflag:=backup;raise e
+	   
 open Genarg
 open Pcoq
 open Pp
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 196f11bf55..aaf195a43a 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -20,7 +20,13 @@ open Libnames
 
 let qflag=ref true
 
-let (+-) i j=if i=0 then j else i
+let (=?) f g i1 i2 j1 j2=
+  let c=f i1 i2 in
+    if c=0 then g j1 j2 else c
+
+let (==?) fg h i1 i2 j1 j2 k1 k2=
+  let c=fg i1 i2 j1 j2 in
+    if c=0 then h k1 k2 else c
 
 type ('a,'b)sum=Left of 'a|Right of 'b
 	
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 1f9d653b2f..1e23d7c0bc 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -14,7 +14,11 @@ open Libnames
 
 val qflag : bool ref
 
-val (+-) : int -> int -> int
+val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
+  'a -> 'a -> 'b -> 'b -> int
+  
+val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> 
+  'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
 
 type ('a,'b) sum = Left of 'a | Right of 'b
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 00a6fe89df..ebd820bcc9 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -95,25 +95,35 @@ let left_or_tac ind id tacrec seq=
       (Array.map f v)
 
 let forall_tac tacrec seq=
-  tclTHEN intro (wrap 0 true tacrec seq)
+  tclTHEN intro (wrap 1 true tacrec seq)
 
-let left_forall_tac i dom atoms internal id tacrec seq=
-  let insts=find_instances i atoms seq in
-    if insts=[] then
-      if internal && not (lookup id None seq) then
-	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]
-      else tclFAIL 0 "no phantom variable for external hyp"
-    else
-      let tac t=
+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(i,dom)-> 
+	     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
@@ -122,29 +132,34 @@ let left_forall_tac i dom atoms internal id tacrec seq=
 	     intro; 
 	     tclSOLVE 
 	       [wrap 1 false tacrec 
-		  (deepen (record id (Some t) seq))]] in
-	tclFIRST (List.map tac insts)
+		  (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 arrow_tac tacrec seq=
   tclTHEN intro (wrap 1 true tacrec seq)
-    
-let exists_tac i dom atoms tacrec seq=
-  let insts=find_instances i atoms seq in
-    if insts=[] then 
-      tclTHENS (cut dom) 
+   
+
+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]
-	 else
-	   let tac t=
-	     tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	       (tclSOLVE [wrap 0 true tacrec (deepen seq)]) in
-	     tclFIRST (List.map tac insts)
-	       
+	    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
+
 let left_exists_tac id tacrec seq=
   tclTHENLIST
     [simplest_elim (constr_of_reference id);
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 7dbd5f556b..692443baed 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -37,11 +37,19 @@ val left_or_tac : inductive -> lseqtac
 
 val forall_tac : seqtac
 
-val left_forall_tac : int -> types -> (bool * constr) list -> bool -> lseqtac
+val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t
+
+val left_instance_tac : Unify.instance * global_reference -> seqtac
+
+val left_forall_tac : Formula.left_formula list -> seqtac
 
 val arrow_tac : seqtac
 
-val exists_tac : int -> types -> (bool * constr) list -> seqtac
+val dummy_exists_tac : constr -> seqtac
+
+val right_instance_tac : constr * int -> seqtac
+
+val exists_tac : (constr * int) list -> seqtac
 	       
 val left_exists_tac : lseqtac
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 678c35a950..1684716d1f 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -52,27 +52,83 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
+(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let rec compare_list f l1 l2=
+  match l1,l2 with
+      [],[]-> 0
+    | [],_ -> -1
+    | _,[] -> 1
+    | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2
+
+
+let compare_array f v1 v2=  
+  let l=Array.length v1 in
+  let c=l - Array.length v2 in
+    if c=0 then
+      let rec comp_aux i=
+	if i<0 then 0 
+	else
+	  let ci=f v1.(i) v2.(i) in
+	    if ci=0 then 
+	      comp_aux (i-1)
+	    else ci
+      in comp_aux (l-1)
+    else c
+
+let compare_constr_int f t1 t2 =
+  match kind_of_term t1, kind_of_term t2 with
+    | Rel n1, Rel n2 -> n1 - n2
+    | Meta m1, Meta m2 -> m1 - m2
+    | Var id1, Var id2 -> Pervasives.compare id1 id2
+    | Sort s1, Sort s2 -> Pervasives.compare s1 s2
+    | Cast (c1,_), _ -> f c1 t2
+    | _, Cast (c2,_) -> f t1 c2
+    | Prod (_,t1,c1), Prod (_,t2,c2) 
+    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+	(f =? f) t1 t2 c1 c2 
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
+	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
+    | App (_,_), App (_,_) ->
+	let c1,l1=decompose_app t1 
+	and c2,l2=decompose_app t2 in
+	  (f =? (compare_list f)) c1 c2 l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> 
+	((-) =? (compare_array f)) e1 e2 l1 l2
+    | Const c1, Const c2 -> Pervasives.compare c1 c2
+    | Ind c1, Ind c2 -> Pervasives.compare c1 c2
+    | Construct c1, Construct c2 -> Pervasives.compare c1 c2
+    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
+	((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2
+    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
+	ln1 ln2 tl1 tl2 bl1 bl2
+    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
+	ln1 ln2 tl1 tl2 bl1 bl2
+    | _ -> Pervasives.compare t1 t2
+
+let rec compare_constr m n=
+  compare_constr_int compare_constr m n
+    
 module OrderedConstr=
 struct
   type t=constr
-  let rec compare c1 c2=
-    match (kind_of_term c1,kind_of_term c2) with
-	(Prod(_,a1,b1),Prod(_,a2,b2))
-      | (Lambda(_,a1,b1),Lambda(_,a2,b2)) ->
-	  (compare a1 a2) +- (compare b1 b2)
-      | (LetIn(_,a1,b1,aa1),LetIn(_,a2,b2,aa2)) ->
- 	  ((compare a1 a2) +- (compare b1 b2)) +- (compare aa1 aa2)
-      | _-> Pervasives.compare c1 c2
+  let compare=compare_constr
 end
 
 module Hitem=
 struct 
   type t=(global_reference * constr option)
   let compare (id1,co1) (id2,co2)=
-    (Pervasives.compare id1 id2) +- 
-    (match co1,co2 with
-	 Some c1,Some c2 -> OrderedConstr.compare c1 c2
-       | _->Pervasives.compare co1 co2)
+    (Pervasives.compare 
+     =? (fun oc1 oc2 ->
+	   match oc1,oc2 with 
+	       Some c1,Some c2 -> OrderedConstr.compare c1 c2
+	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
 end
 
 module CM=Map.Make(OrderedConstr)
@@ -185,7 +241,6 @@ let create_with_auto_hints depth gl=
     !seqref
 
 let print_cmap map=
-  
   let print_entry c l s=
     let xc=Constrextern.extern_constr false (Global.env ()) c in
       str "| " ++ 
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 751c297453..851396d45a 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -19,6 +19,8 @@ val right_reversible : right_pattern -> bool
 	
 val left_reversible : left_pattern -> bool
 
+module OrderedConstr: Set.OrderedType with type t=constr
+
 module CM: Map.S with type key=constr
 
 module History: Set.S with type elt = global_reference * constr option
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 0c336b6d31..5c0148d1f1 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -13,6 +13,7 @@ open Formula
 open Sequent
 open Tacmach
 open Term
+open Names
 open Termops
 open Reductionops
 
@@ -80,71 +81,161 @@ let unif t1 t2= (* Martelli-Montanari style *)
       assert false 
 	(* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
-      
+
 (* collect tries finds ground instantiations for Meta i*)
 let is_ground t=(Clenv.collect_metas t)=[]
 
-let collect i l=
-  try
-    let t=List.assoc i l in 
-      if is_ground t then Some t else None
-  with Not_found->None
+let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
 
-let value i=
+let value i t=
+  let add x y=
+    if x<0 then y else if y<0 then x else x+y in
   let tref=mkMeta i in
   let rec vaux term=
-    if term=tref then 1 else 
-      let f v t=max v (vaux t) in
-      let vrec=fold_constr f 0 term in
-	if vrec=0 then 0 else succ vrec in vaux
+    if term=tref then 0 else 
+      let f v t=add v (vaux t) in
+      let vr=fold_constr f (-1) term in
+	if vr<0 then -1 else vr+1 in
+    vaux t
+	  
+type instance=
+    Real of constr*int (* instance*valeur heuristique*)
+  | Phantom of constr (* domaine de quantification *)
+ 	  
+let unif_atoms i dom t1 t2=
+  if is_head_meta t1 || is_head_meta t2  then None else
+    try 
+      let t=List.assoc i (unif t1 t2) in 
+	if is_ground t then Some (Real(t,value i t1))
+	else if is_head_meta t then Some (Phantom dom)
+	else None
+    with
+	UFAIL(_,_) ->None
+      | Not_found ->Some (Phantom dom)
+      
+let compare_instance inst1 inst2=
+	match inst1,inst2 with
+	    Phantom(d1),Phantom(d2)->
+	      (OrderedConstr.compare d1 d2)
+	  | Real(c1,n1),Real(c2,n2)->
+	      ((-) =? OrderedConstr.compare) n2 n1 c1 c2
+	  | Phantom(_),_-> 1
+	  | _,_-> -1
 
-let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
+module OrderedRightInstance=
+struct 
+  type t = constr*int
+  let compare (c1,n1) (c2,n2) = ((-) =? OrderedConstr.compare) n2 n1 c1 c2
+end
 
-let unif_atoms_for_meta i (b1,t1) (b2,t2)=
-  if b1=b2  || is_head_meta t1 || is_head_meta t2  then None else
-    try 
-       match collect i (unif t1 t2) with
-	   None->None
-	 | Some t->Some ((max (value i t1) (value i t2)),t)
-    with UFAIL(_,_) ->None
-    
-module OrderedConstr=
+module OrderedLeftInstance=
 struct
-  type t=int*constr
-  let compare (n1,t1) (n2,t2)=
-    (n2 - n1) +- (Pervasives.compare t1 t2) 
-    (* we want a decreasing total order *)
+  type t=instance * Libnames.global_reference
+  let compare (inst1,id1) (inst2,id2)=
+    (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2
+    (* we want a __decreasing__ total order *)
 end
   
-module CS=Set.Make(OrderedConstr)
+module RIS=Set.Make(OrderedRightInstance)
+module LIS=Set.Make(OrderedLeftInstance)
   
-let match_atom_list i atom l=
-  let f atom2 accu=
-    match unif_atoms_for_meta i atom atom2 with
-	None-> accu
-      | Some t-> CS.add t accu in
-    List.fold_right f l CS.empty
-
-let match_lists i l1 l2=
-  let f atom accu=
-    CS.union (match_atom_list i atom l2) accu in
-    List.fold_right f l1 CS.empty
-      
-let find_instances i l seq=
-  let match_hyp f accu=
-    CS.union 
-      (if f.internal then 
-	 match_lists i l f.atoms 
-       else 
-	 CS.empty) 
-      accu in
-  let match_atom t accu=
-    CS.union (match_atom_list i (false,t) l) accu in
-  let s1=
-    match seq.gl with 
-	Atomic t->(match_atom_list i (true,t) l)
-      | Complex(_,_,l1)->(match_lists i l l1) in
-  let s2=List.fold_right match_atom seq.latoms s1 in
-  let s3=HP.fold match_hyp seq.redexes s2 in
-    List.map snd (CS.elements s3)
+(* le premier argument est une sous formule a instancier *)
+
+let match_atom_with_latoms i dom (pol,atom) latoms accu=
+  if pol then 
+    let f latom accu=
+      match unif_atoms i dom atom latom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some (Real(t,i)) ->(false,RIS.add (t,i) (snd accu)) in
+      List.fold_right f latoms accu
+  else accu 
+
+let match_atom_with_hyp_atoms i dom (pol,atom) lf accu=
+  let f (b,hatom) accu=
+    if b=pol then accu else
+      match unif_atoms i dom atom hatom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some (Real(t,i))->(false,RIS.add (t,i) (snd accu)) in
+    List.fold_right f lf.atoms accu
+
+let match_atom_with_goal i dom (pol,atom) glatoms accu=
+  let f (b,glatom) accu=
+    if b=pol then accu else
+      match unif_atoms i dom atom glatom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some (Real(t,i)) ->(false,RIS.add (t,i) (snd accu)) in
+    List.fold_right f glatoms accu
+
+let give_right_instances i dom ratoms seq=
+  let f ratom accu=
+    let accu1= match_atom_with_goal i dom ratom ratoms accu in
+    let accu2=
+      match_atom_with_latoms i dom ratom seq.latoms accu1 in
+      HP.fold (match_atom_with_hyp_atoms i dom ratom) seq.redexes accu2 in
+  let (b,accu0)=List.fold_right f ratoms (false,RIS.empty) in
+    if b & RIS.is_empty accu0 then 
+      None
+    else
+      Some (RIS.elements accu0)
+
+(*left*) 
+	  
+let match_named_atom_with_latoms id i dom (pol,atom) latoms accu=
+  if pol then 
+    let f latom accu=
+      match unif_atoms i dom atom latom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some inst ->(false,LIS.add (inst,id) (snd accu)) in
+      List.fold_right f latoms accu
+  else accu 
+
+let match_named_atom_with_hyp_atoms id i dom (pol,atom) lf accu=
+  let f (b,hatom) accu=
+    if b=pol then accu else
+      match unif_atoms i dom atom hatom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some inst->(false,LIS.add (inst,id) (snd accu)) in
+    List.fold_right f lf.atoms accu
+
+let match_named_atom_with_goal id i dom (pol,atom) gl accu=
+  match gl with 
+      Atomic t->
+	if pol then accu else
+	  (match unif_atoms i dom atom t with
+	       None->accu
+	     | Some (Phantom _) ->(true,snd accu)
+	     | Some inst ->(false,LIS.add (inst,id) (snd accu)))
+    | Complex (_,_,glatoms)->
+	let f (b,glatom) accu=
+	  if b=pol then accu else
+	    match unif_atoms i dom atom glatom with
+		None->accu
+	      | Some (Phantom _) ->(true,snd accu)
+	      | Some inst ->(false,LIS.add (inst,id) (snd accu)) in
+	  List.fold_right f glatoms accu
+
+let match_one_forall_hyp seq lf accu=
+  match lf.pat with 
+      Lforall(i,dom)->
+	let f latom accu=
+	  let accu1=match_named_atom_with_goal lf.id i dom latom seq.gl accu in
+	  let accu2=
+	    match_named_atom_with_latoms lf.id i dom latom seq.latoms accu1 in
+	    HP.fold (match_named_atom_with_hyp_atoms lf.id i dom latom) 
+	      seq.redexes accu2 in
+	let (b,accu0)=List.fold_right f lf.atoms (false,LIS.empty) in
+	  if b & LIS.is_empty accu0 then 
+	    LIS.add (Phantom dom,lf.id) accu
+	  else
+	    LIS.union accu0 accu
+    | _ ->anomaly "can't happen" 
+
+let give_left_instances lfh seq=
+  LIS.elements (List.fold_right (match_one_forall_hyp seq) lfh LIS.empty)
 
+(* TODO: match with goal *)
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 5423884886..281e940630 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -8,9 +8,17 @@
 
 (* $Id$ *)
 
+open Libnames
 open Term
 
-val unif_atoms_for_meta : int -> (bool * constr) -> (bool * constr) ->
-  (int*constr) option
+type instance=
+    Real of constr*int (* instance*valeur heuristique*)
+  | Phantom of constr (* domaine de quantification *)
 
-val find_instances : int -> (bool * constr) list -> Sequent.t -> constr list
+val unif_atoms : int -> constr -> constr -> constr -> instance option
+  
+val give_right_instances : int -> constr -> (bool * constr) list -> 
+  Sequent.t -> (constr*int) list option
+
+val give_left_instances : Formula.left_formula list-> Sequent.t -> 
+  (instance*global_reference) list