Major Ground update, may break semantics

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

9 files changed, 298 insertions, 310 deletions

diff --git a/.depend.newcoq b/.depend.newcoq
index 70a37e7d3c..9cdc3b1da4 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -153,12 +153,6 @@ newtheories/Sets/Multiset.vo: newtheories/Sets/Multiset.v newtheories/Sets/Permu
 newtheories/Sets/Relations_3_facts.vo: newtheories/Sets/Relations_3_facts.v newtheories/Sets/Relations_1.vo newtheories/Sets/Relations_1_facts.vo newtheories/Sets/Relations_2.vo newtheories/Sets/Relations_2_facts.vo newtheories/Sets/Relations_3.vo
 newtheories/Sets/Partial_Order.vo: newtheories/Sets/Partial_Order.v newtheories/Sets/Ensembles.vo newtheories/Sets/Relations_1.vo
 newtheories/Sets/Uniset.vo: newtheories/Sets/Uniset.v newtheories/Bool/Bool.vo newtheories/Sets/Permut.vo
-newtheories/FSets/FSet.vo: newtheories/FSets/FSet.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetBridge.vo newtheories/FSets/FSetProperties.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetRBT.vo
-newtheories/FSets/FSetList.vo: newtheories/FSets/FSetList.v newtheories/FSets/FSetInterface.vo
-newtheories/FSets/FSetBridge.vo: newtheories/FSets/FSetBridge.v newtheories/FSets/FSetInterface.vo
-newtheories/FSets/FSetProperties.vo: newtheories/FSets/FSetProperties.v newcontrib/omega/Omega.vo newtheories/FSets/FSetInterface.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Bool/Zerob.vo
-newtheories/FSets/FSetInterface.vo: newtheories/FSets/FSetInterface.v newtheories/Bool/Bool.vo newtheories/Lists/PolyList.vo newtheories/Sorting/Sorting.vo newtheories/Setoids/Setoid.vo
-newtheories/FSets/FSetRBT.vo: newtheories/FSets/FSetRBT.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetBridge.vo newcontrib/omega/Omega.vo newtheories/ZArith/ZArith.vo
 newtheories/IntMap/Adalloc.vo: newtheories/IntMap/Adalloc.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/Arith/Arith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo
 newtheories/IntMap/Mapcanon.vo: newtheories/IntMap/Mapcanon.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo
 newtheories/IntMap/Addec.vo: newtheories/IntMap/Addec.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 156ef7ae24..3cf0997733 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -123,6 +123,8 @@ type atoms = {positive:constr list;negative:constr list}
 
 let no_atoms = (false,{positive=[];negative=[]})
 
+let dummy_id=VarRef (id_of_string "")
+
 let build_atoms gl metagen polarity cciterm =
   let trivial =ref false
   and positive=ref []
@@ -171,17 +173,14 @@ let build_atoms gl metagen polarity cciterm =
 
        
 type right_pattern =
-    Rand
+    Rarrow
+  | Rand
   | Ror 
+  | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-  | Rarrow
   | Revaluable of evaluable_global_reference
-      
-type right_formula =
-    Complex of right_pattern*constr*atoms
-  | Atomic of constr
-      
+   
 type left_arrow_pattern=
     LLatom
   | LLfalse of inductive*constr list
@@ -201,46 +200,62 @@ type left_pattern=
   | Levaluable of evaluable_global_reference
   | LA of constr*left_arrow_pattern
 
-type left_formula={id:global_reference;
-		   constr:constr;
-		   pat:left_pattern;
-		   atoms:atoms;
-		   internal:bool}
+type t={id:global_reference;
+	constr:constr;
+	pat:(left_pattern,right_pattern) sum;
+	atoms:atoms}
     
-let build_left_entry nam typ internal gl metagen=
+let build_formula side nam typ gl metagen=
   try 
     let m=meta_succ(metagen false) in
     let trivial,atoms=
       if !qflag then 
-	build_atoms gl metagen false typ 
+	build_atoms gl metagen side typ 
       else no_atoms in
     let pattern=
-      match kind_of_formula gl typ with
-	  False(i,_)        ->  Lfalse
-	| Atom a       ->  raise (Is_atom a)
-	| And(i,_)         ->  Land i
-	| Or(i,_)          ->  Lor i
-	| Exists (ind,_) ->  Lexists ind 
-	| Forall (d,_) -> 
-	    Lforall(m,d,trivial)
-	| Evaluable (egc,_) ->Levaluable egc 
-	| Arrow (a,b) ->LA (a, 
-			    match kind_of_formula gl a with
-				False(i,l)-> LLfalse(i,l)
-			      | Atom t->     LLatom
-			      | And(i,l)->      LLand(i,l)
-			      | Or(i,l)->       LLor(i,l)
-			      | Arrow(a,c)-> LLarrow(a,c,b)
-			      | Exists(i,l)->LLexists(i,l)
-			      | Forall(_,_)->LLforall a
-			      | Evaluable (egc,_)-> LLevaluable egc) in
+      if side then
+	let pat=
+	  match kind_of_formula gl typ with
+	      False(_,_)        -> Rfalse
+	    | Atom a       -> raise (Is_atom a)
+	    | And(_,_)        -> Rand
+	    | Or(_,_)         -> Ror
+	    | Exists (i,l) -> 
+		let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
+		  Rexists(m,d,trivial)
+	    | Forall (_,a) -> Rforall 
+	    | Arrow (a,b) -> Rarrow 
+	    | Evaluable (egc,_)->Revaluable egc in
+	  Right pat
+      else
+	let pat=
+	  match kind_of_formula gl typ with
+	      False(i,_)        ->  Lfalse
+	    | Atom a       ->  raise (Is_atom a)
+	    | And(i,_)         ->  Land i
+	    | Or(i,_)          ->  Lor i
+	    | Exists (ind,_) ->  Lexists ind 
+	    | Forall (d,_) -> 
+		Lforall(m,d,trivial)
+	    | Evaluable (egc,_) ->Levaluable egc 
+	    | Arrow (a,b) ->LA (a, 
+				match kind_of_formula gl a with
+				    False(i,l)-> LLfalse(i,l)
+				  | Atom t->     LLatom
+				  | And(i,l)->      LLand(i,l)
+				  | Or(i,l)->       LLor(i,l)
+				  | Arrow(a,c)-> LLarrow(a,c,b)
+				  | Exists(i,l)->LLexists(i,l)
+				  | Forall(_,_)->LLforall a
+				  | Evaluable (egc,_)-> LLevaluable egc) in
+	  Left pat
+    in
       Left {id=nam;
 	    constr=typ;
 	    pat=pattern;
-	    atoms=atoms;
-	    internal=internal}
+	    atoms=atoms}
   with Is_atom a-> Right a
-    
+(*    
 let build_right_entry typ gl metagen=
   try
     let m=meta_succ(metagen false) in 
@@ -262,4 +277,4 @@ let build_right_entry typ gl metagen=
 	| Evaluable (egc,_)->Revaluable egc in
       Complex(pattern,typ,atoms)
   with Is_atom a-> Atomic a
-
+*)
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 7b5e9d826a..815657f543 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -31,7 +31,7 @@ val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array
 val match_with_evaluable : Proof_type.goal Tacmach.sigma ->
   constr -> (evaluable_global_reference * constr) option
 
-type kind_of_formula=
+type kind_of_formula =
     Arrow of constr*constr
   | False of inductive*constr list
   | And of inductive*constr list
@@ -45,22 +45,21 @@ val kind_of_formula : Proof_type.goal Tacmach.sigma ->
   constr -> kind_of_formula
 
 type atoms = {positive:constr list;negative:constr list}
+
+val dummy_id: global_reference
 			
 val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
   bool -> constr -> bool * atoms
 
 type right_pattern =
-    Rand
+    Rarrow
+  | Rand
   | Ror 
+  | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-  | Rarrow
   | Revaluable of Names.evaluable_global_reference
     
-type right_formula =
-    Complex of right_pattern*constr*atoms
-  | Atomic of constr
-      
 type left_arrow_pattern=
     LLatom
   | LLfalse of inductive*constr list
@@ -80,17 +79,13 @@ type left_pattern=
   | Levaluable of Names.evaluable_global_reference
   | LA of constr*left_arrow_pattern
       
-type left_formula={id:global_reference;
-		   constr:constr;
-		   pat:left_pattern;
-		   atoms:atoms;
-		   internal:bool}
-
+type t={id: global_reference;
+	constr: constr;
+	pat: (left_pattern,right_pattern) sum;
+	atoms: atoms}
+    
 (*exception Is_atom of constr*)
 
-val build_left_entry : 
-  global_reference -> types -> bool -> Proof_type.goal Tacmach.sigma ->
-  counter -> (left_formula,types) sum
+val build_formula : bool -> global_reference -> types -> 
+  Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
 
-val build_right_entry : types -> Proof_type.goal Tacmach.sigma -> 
-  counter -> right_formula
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index b8f6849772..4fbc68c0c6 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -42,106 +42,104 @@ let _=
     declare_int_option gdopt
       
 let ground_tac solver startseq gl=
-  let rec toptac seq gl=
+  let rec toptac ctx seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
     then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
-    match seq.gl with 
-	Atomic t->
-	  tclORELSE (axiom_tac t seq) (left_tac seq []) gl
-      | Complex (pat,t,l)->
-	  tclORELSE (axiom_tac t seq)
-	  (match pat with
-	       Rand->
-		 and_tac toptac seq
-	     | Rforall->
-		 forall_tac toptac seq
-	     | Rarrow->
-		 arrow_tac toptac seq
-	     | Revaluable egr->
-		 evaluable_tac egr toptac seq
-	     | _->
-		 if not (is_empty_left seq) && rev_left seq then 
-		   left_tac seq [] 
-		 else 
-		   right_tac seq []) gl
-  and right_tac seq ctx gl=
-    let re_add s=re_add_left_list ctx s in
-      match seq.gl with
-	  Atomic _ -> left_tac seq ctx gl
-	| Complex (pat,_,atoms)->
-	    match pat with
-		 Ror->
-		   tclORELSE
-		   (or_tac toptac (re_add seq))
-		   (left_tac seq ctx) gl
-	       | Rexists(i,dom,triv)->
-		   let cont_tac=left_tac seq ctx in
-		     if seq.depth<=0 || not !qflag then 
-		       cont_tac gl
-		     else 
-		       (match 
-			  Instances.give_right_instances i dom triv 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 
-      solver gl
-    else 
-      let (hd,seq1)=take_left seq in 
-      let re_add s=re_add_left_list ctx s in 
-	match hd.pat with
-	    Lfalse->
-	      left_false_tac hd.id gl
-	  | Land ind->
-	      left_and_tac ind hd.id toptac (re_add seq1) gl
-	  | Lor ind->
-	      left_or_tac ind hd.id toptac (re_add seq1) gl
-	  | Lforall (_,_,_)->
-	      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 ind ->
-	      if !qflag then
-		left_exists_tac ind hd.id toptac (re_add seq1) gl
-	      else (left_tac seq1 (hd::ctx)) gl
-	  | Levaluable egr->
-	      left_evaluable_tac egr hd.id toptac (re_add seq1) gl
-	  | LA (typ,lap)->
-	      tclORELSE
-	      (ll_atom_tac typ hd.id toptac (re_add seq1))
-	      (match lap with
-		   LLatom->
-		     right_tac seq1 (hd::ctx) 
-		 | LLfalse (ind,largs) | LLand (ind,largs) | LLor(ind,largs) ->
-		     ll_ind_tac ind largs hd.id toptac (re_add seq1) 
-		 | LLforall p ->	      
-		     tclORELSE
-		     (if seq.depth<=0 || not !qflag then 
-			tclFAIL 0 "max depth" 
-		      else 
-			ll_forall_tac p hd.id toptac (re_add seq1))
-		     (left_tac seq1 (hd::ctx))
-		 | LLexists (ind,l) ->
-		     if !qflag then
-		       ll_ind_tac ind l hd.id toptac (re_add seq1) 
-		     else
-		       left_tac seq1 (hd::ctx)
-		 | LLarrow (a,b,c) ->	      
-		     tclORELSE
-		     (ll_arrow_tac a b c hd.id toptac (re_add seq1))
-		     (left_tac seq1 (hd::ctx))
-		 | LLevaluable egr->
-		     left_evaluable_tac egr hd.id toptac (re_add seq1)) gl in
-    wrap (List.length (pf_hyps gl)) true toptac (startseq gl) gl
+    tclORELSE (axiom_tac seq.gl seq)
+      begin
+	try      
+	  let (hd,seq1)=take_formula seq  
+	  and re_add s=re_add_formula_list ctx s in
+	  let continue=toptac [] 
+	  and backtrack=toptac (hd::ctx) seq1  in
+	    match hd.pat with
+		Right rpat->
+		  begin
+		    match rpat with
+			Rand->
+			  and_tac continue seq1
+		      | Rforall->
+			  forall_tac continue seq1
+		      | Rarrow->
+			  arrow_tac continue seq1
+		      | Revaluable egr->
+			  evaluable_tac egr continue seq1
+		      | Ror->
+			  tclORELSE
+			  (or_tac continue (re_add seq1))
+			  backtrack
+		      | Rfalse->backtrack 
+		      | Rexists(i,dom,triv)->
+			  let (lfp,seq2)=collect_quantified seq in
+			    tclORELSE
+			      (if seq.depth<=0 || not !qflag then 
+				 tclFAIL 0 "max depth" 
+			       else 
+				 quantified_tac lfp continue (re_add seq))
+			      (toptac (lfp@ctx) seq2)
+			      (* need special backtracking *)
+		  end
+	      | Left lpat->
+		  begin
+		    match lpat with
+			Lfalse->
+			  left_false_tac hd.id
+		      | Land ind->
+			  left_and_tac ind hd.id continue (re_add seq1)
+		      | Lor ind->
+			  left_or_tac ind hd.id continue (re_add seq1)
+		      | Lforall (_,_,_)->
+			  let (lfp,seq2)=collect_quantified seq in
+			    tclORELSE
+			      (if seq.depth<=0 || not !qflag then 
+				 tclFAIL 0 "max depth" 
+			       else 
+				 quantified_tac lfp continue (re_add seq))
+			      (toptac (lfp@ctx) seq2)
+			      (* need special backtracking *)
+		      | Lexists ind ->
+			  if !qflag then
+			    left_exists_tac ind hd.id continue (re_add seq1)
+			  else backtrack
+		      | Levaluable egr->
+			  left_evaluable_tac egr hd.id continue (re_add seq1)
+		      | LA (typ,lap)->
+			  tclORELSE
+			  (ll_atom_tac typ hd.id continue (re_add seq1))
+			  begin
+			    match lap with
+				LLatom -> backtrack 
+			      | LLand (ind,largs) | LLor(ind,largs) 
+			      | LLfalse (ind,largs)->
+				  ll_ind_tac ind largs hd.id continue 
+				  (re_add seq1) 
+			      | LLforall p ->	      
+				  tclORELSE
+				  (if seq.depth<=0 || not !qflag then 
+				     tclFAIL 0 "max depth" 
+				   else 
+				     ll_forall_tac p hd.id continue 
+				       (re_add seq1))
+				  backtrack
+			      | LLexists (ind,l) ->
+				  if !qflag then
+				    ll_ind_tac ind l hd.id continue 
+				      (re_add seq1)
+				  else
+				    backtrack
+			      | LLarrow (a,b,c) ->	      
+				  tclORELSE
+				  (ll_arrow_tac a b c hd.id continue 
+				     (re_add seq1))
+				  backtrack
+			      | LLevaluable egr->
+				  left_evaluable_tac egr hd.id continue 
+				  (re_add seq1)
+			  end
+		  end
+	    with Heap.EmptyHeap->solver
+      end gl in
+    wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
       
 let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
     
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index e38af4c0c9..41a4078cc3 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -39,36 +39,34 @@ let compare_instance inst1 inst2=
 	    Phantom(d1),Phantom(d2)->
 	      (OrderedConstr.compare d1 d2)
 	  | Real((m1,c1),n1),Real((m2,c2),n2)->
-	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n2 n1 c1 c2
+	      ((-) =? (-) ==? OrderedConstr.compare) m1 m2 n1 n2 c1 c2
 	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
 	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
 
-module OrderedRightInstance=
-struct 
-  type t = instance
-  let compare = compare_instance
-end
+let compare_gr id1 id2=
+  if id1==id2 then 0 else
+    if id1==dummy_id then 1 
+    else if id2==dummy_id then -1 
+    else Pervasives.compare id1 id2
 
-module OrderedLeftInstance=
+module OrderedInstance=
 struct
   type t=instance * Libnames.global_reference
   let compare (inst1,id1) (inst2,id2)=
-    (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2
+    (compare_instance =? compare_gr) inst2 inst1 id2 id1
     (* we want a __decreasing__ total order *)
 end
   
-module RIS=Set.Make(OrderedRightInstance)
-module LIS=Set.Make(OrderedLeftInstance)
-
-let make_goal_atoms seq=
-  match seq.gl with
-      Atomic t->{negative=[];positive=[t]}
-    | Complex (_,_,l)->l 
+module IS=Set.Make(OrderedInstance)
 
-let make_left_atoms seq=
-    {negative=seq.latoms;positive=[]}
+let make_simple_atoms seq=
+  let ratoms=
+    match seq.glatom with
+	Some t->[t]
+      | None->[]
+  in {negative=seq.latoms;positive=ratoms}
 
-let do_sequent setref triv add mkelt seq i dom atoms=
+let do_sequent setref triv id seq i dom atoms=
   let flag=ref true in
   let phref=ref triv in
   let do_atoms a1 a2 =
@@ -76,47 +74,38 @@ let do_sequent setref triv add mkelt seq i dom atoms=
       match unif_atoms i dom t1 t2 with
 	  None->()
 	| Some (Phantom _) ->phref:=true
-	| Some c ->flag:=false;setref:=add (mkelt c) !setref in
+	| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
       List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
       List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
     HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
-    do_atoms atoms (make_left_atoms seq);
-    do_atoms atoms (make_goal_atoms seq);
+    do_atoms atoms (make_simple_atoms seq);
     !flag && !phref 
  
-let give_right_instances i dom triv atoms seq=
-  let setref=ref RIS.empty in
-  let inj inst=inst in
-  if do_sequent setref triv RIS.add inj seq i dom atoms then
-    None
-  else
-    Some (RIS.elements !setref)
-
-let match_one_forall_hyp setref seq lf=
+let match_one_quantified_hyp setref seq lf=
   match lf.pat with 
-      Lforall(i,dom,triv)->
-	let inj x=(x,lf.id) in
-	  if do_sequent setref triv LIS.add inj seq i dom lf.atoms then
-	    setref:=LIS.add ((Phantom dom),lf.id) !setref 
+      Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
+	if do_sequent setref triv lf.id seq i dom lf.atoms then
+	  setref:=IS.add ((Phantom dom),lf.id) !setref 
     | _ ->anomaly "can't happen" 
 
-let give_left_instances lfh seq=
-  let setref=ref LIS.empty in
-    List.iter (match_one_forall_hyp setref seq) lfh;
-    LIS.elements !setref
+let give_instances lf seq=
+  let setref=ref IS.empty in
+    List.iter (match_one_quantified_hyp setref seq) lf;
+    IS.elements !setref
 	  	  
-(*tactics*)
+(* collector for the engine *)
 
-
-let rec collect_forall seq=
-  if is_empty_left seq then ([],seq) 
-  else
-    let hd,seq1=take_left seq in
+let rec collect_quantified seq=
+  try
+    let hd,seq1=take_formula seq in
       (match hd.pat with 
-	   Lforall(_,_,_)-> 
-	     let (q,seq2)=collect_forall seq1 in
+	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> 
+	     let (q,seq2)=collect_quantified seq1 in
 	       ((hd::q),seq2)
 	 | _->[],seq)
+  with Heap.EmptyHeap -> [],seq
+
+(* tactics   *)
 
 let left_instance_tac (inst,id) tacrec seq=
   match inst with
@@ -145,11 +134,9 @@ let left_instance_tac (inst,id) tacrec seq=
 	       [wrap 1 false tacrec 
 		  (deepen (record (id,Some c) 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=
+let right_instance_tac inst tacrec seq=
+  match inst with
+      Phantom dom ->
 	tclTHENS (cut dom) 
 	[tclTHENLIST
 	   [intro;
@@ -158,17 +145,18 @@ let dummy_exists_tac dom  tacrec seq=
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
 	 tclTRY assumption] 
- 
-let right_instance_tac inst tacrec seq=
-  match inst with
-      Phantom _ ->anomaly "can't happen" 
     | Real ((m,t),_) ->
 	if m>0 then tclFAIL 0 "not implemented ... yes"
 	else
-	tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	(tclSOLVE [wrap 0 true tacrec (deepen 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 instance_tac inst=
+  if (snd inst)==dummy_id then 
+    right_instance_tac (fst inst)
+  else
+    left_instance_tac inst
 
+let quantified_tac lf tacrec seq gl=
+  let insts=give_instances lf seq in
+    tclFIRST (List.map (fun inst->instance_tac inst tacrec seq) insts) gl
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
index b1d88280b9..ed85308cd2 100644
--- a/contrib/first-order/instances.mli
+++ b/contrib/first-order/instances.mli
@@ -14,26 +14,9 @@ open Names
 open Libnames
 open Rules
   
-val give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> 
-  Sequent.t -> Unify.instance list option
-
-val give_left_instances : Formula.left_formula list-> Sequent.t -> 
-  (Unify.instance*global_reference) list
-
-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 dummy_exists_tac : constr -> seqtac
-
-val right_instance_tac : Unify.instance -> seqtac
-
-val exists_tac : Unify.instance list -> seqtac
-	       
-
+val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
 
+val quantified_tac : Formula.t list -> seqtac
 
 
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index c5c7319e8d..e7b71f54fd 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -38,9 +38,10 @@ let wrap n b tacrec seq gls=
 	      List.exists (occur_var_in_decl env id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_left (VarRef id,typ) (aux (i-1) q (nd::ctx)) true gls in
+	      add_formula false (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
-  let seq2=if b then change_right (pf_concl gls) seq1 gls else seq1 in
+  let seq2=if b then 
+    add_formula true dummy_id (pf_concl gls) seq1 gls else seq1 in
     tacrec seq2 gls
 
 let id_of_global=function
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index c63c10f43a..4942503c6a 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -21,34 +21,43 @@ let newcnt ()=
   let cnt=ref (-1) in
     fun b->if b then incr cnt;!cnt
 
-let priority = function (* pure heuristics, <=0 for non reversible *)
-      Lfalse             ->1000
-    | Land _             ->  90
-    | Lor _              ->  40
-    | Lforall (_,_,_)      -> -30 (* must stay at lowest priority *)
-    | Lexists _           ->  60
-    | Levaluable _       -> 100
-    | LA(_,lap) ->
-	match lap with
-	    LLatom             ->   0
-	  | LLfalse (_,_)      -> 100
-	  | LLand (_,_)        ->  80
-	  | LLor (_,_)         ->  70
-	  | LLforall _         -> -20
-	  | LLexists (_,_)     ->  50
-	  | LLarrow  (_,_,_)   -> -10 
-	  | LLevaluable _      -> 100
-
-let right_reversible=
+let priority = (* pure heuristics, <=0 for non reversible *)
   function
-      Rarrow | Rand | Rforall | Revaluable _ ->true
-    | _ ->false
-	
+      Right rf->
+	begin
+	  match rf with
+	      Rarrow ->          100
+	    | Rand ->             40 
+	    | Ror ->             -15
+	    | Rfalse ->          -50 (* dead end for sure *)
+	    | Rforall ->         100
+	    | Revaluable _ ->    100 
+	    | Rexists (_,_,_) -> -30
+	end
+    | Left lf ->
+	match lf with
+	    Lfalse             ->  1000 (* yipee ! *)
+	  | Land _             ->    90
+	  | Lor _              ->    40
+	  | Lforall (_,_,_)      -> -30 (* must stay at lowest priority *)
+	  | Lexists _           ->   60
+	  | Levaluable _       ->   100
+	  | LA(_,lap) ->
+	      match lap with
+		  LLatom             ->   0
+		| LLfalse (_,_)      -> 100
+		| LLand (_,_)        ->  80
+		| LLor (_,_)         ->  70
+		| LLforall _         -> -20
+		| LLexists (_,_)     ->  50
+		| LLarrow  (_,_,_)   -> -10 
+		| LLevaluable _      -> 100
+
 let left_reversible lpat=(priority lpat)>0
 
 module OrderedFormula=
 struct
-  type t=left_formula
+  type t=Formula.t
   let compare e1 e2=
 	(priority e1.pat) - (priority e2.pat)
 end
@@ -65,7 +74,6 @@ let rec compare_list f l1 l2=
     | _,[] -> 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
@@ -160,7 +168,8 @@ type t=
     {redexes:HP.t;
      context:(global_reference list) CM.t;
      latoms:constr list;
-     gl:right_formula;
+     gl:types;
+     glatom:constr option;
      cnt:counter;
      history:History.t;
      depth:int}
@@ -180,49 +189,65 @@ let lookup item seq=
 	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
 	  History.exists p seq.history
 
-let add_left (nam,t) seq internal gl=
-  match build_left_entry nam t internal gl seq.cnt with
-      Left f->{seq with 
-		 redexes=HP.add f seq.redexes;
-		 context=cm_add f.constr nam seq.context}
-    | Right t->{seq with 
-		  context=cm_add t nam seq.context;
-		  latoms=t::seq.latoms}
-
-let re_add_left_list lf seq=
+let add_formula side nam t seq gl=
+  match build_formula side nam t gl seq.cnt with
+      Left f->
+	if side then
+	  {seq with 
+	     redexes=HP.add f seq.redexes;
+	     gl=f.constr;
+	     glatom=None}
+	else
+	  {seq with 
+	     redexes=HP.add f seq.redexes;
+	     context=cm_add f.constr nam seq.context}
+    | Right t->
+	if side then
+	  {seq with gl=t;glatom=Some t}
+	else
+	  {seq with 
+	     context=cm_add t nam seq.context;
+	     latoms=t::seq.latoms}
+
+let re_add_formula_list lf seq=
+  let do_one f cm=
+    if f.id == dummy_id then cm
+    else cm_add f.constr f.id cm in
   {seq with 
      redexes=List.fold_right HP.add lf seq.redexes;
-     context=List.fold_right 
-	       (fun f cm->cm_add f.constr f.id cm) lf seq.context}
-
-let change_right t seq gl=
-  {seq with gl=build_right_entry t gl seq.cnt}
+     context=List.fold_right do_one lf seq.context}
 
 let find_left t seq=List.hd (CM.find t seq.context)
 
-let rev_left seq=
+(*let rev_left seq=
   try
     let lpat=(HP.maximum seq.redexes).pat in
       left_reversible lpat
   with Heap.EmptyHeap -> false
-
-let is_empty_left seq=
+*)
+let no_formula seq=
   seq.redexes=HP.empty
 
-let take_left seq=
+let rec take_formula seq=
   let hd=HP.maximum seq.redexes
   and hp=HP.remove seq.redexes in
-    hd,{seq with 
-	  redexes=hp;
-	  context=cm_remove hd.constr hd.id seq.context}
-
-let take_right seq=seq.gl
-
+    if hd.id == dummy_id then
+      let nseq={seq with redexes=hp} in
+	if seq.gl==hd.constr then 
+	  hd,nseq
+	else
+	  take_formula nseq (* discarding deprecated goal *)
+    else
+      hd,{seq with 
+	    redexes=hp;
+	    context=cm_remove hd.constr hd.id seq.context}
+	
 let empty_seq depth=
   {redexes=HP.empty;   
    context=CM.empty;
    latoms=[];
-   gl=Atomic (mkMeta 1);
+   gl=(mkMeta 1);
+   glatom=None;
    cnt=newcnt ();
    history=History.empty;
    depth=depth}
@@ -231,7 +256,7 @@ let create_with_ref_list l depth gl=
   let f gr seq=
     let c=constr_of_reference gr in    
     let typ=(pf_type_of gl c) in
-      add_left (gr,typ) seq false gl in
+      add_formula false gr typ seq gl in
     List.fold_right f l (empty_seq depth)
 
 open Auto
@@ -245,7 +270,7 @@ let create_with_auto_hints depth gl=
 	  (try 
 	     let gr=reference_of_constr c in 
 	     let typ=(pf_type_of gl c) in
-	       seqref:=add_left (gr,typ) !seqref false gl
+	       seqref:=add_formula false  gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
   let g _ l=List.iter f l in
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 79cf0d1ed9..26c3a95bd7 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -15,10 +15,6 @@ open Tacmach
 open Names
 open Libnames
 
-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
@@ -33,12 +29,13 @@ val cm_add : constr -> global_reference -> global_reference list CM.t ->
 val cm_remove : constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
 
-module HP: Heap.S with type elt=left_formula
+module HP: Heap.S with type elt=Formula.t
 
 type t = {redexes:HP.t;
 	  context: global_reference list CM.t;
 	  latoms:constr list;
-	  gl:right_formula;
+	  gl:types;
+	  glatom:constr option;
 	  cnt:counter;
 	  history:History.t;
 	  depth:int}
@@ -49,22 +46,14 @@ val record: h_item -> t -> t
 
 val lookup: h_item -> t -> bool
 
-val add_left : global_reference * constr -> t -> bool -> 
+val add_formula : bool -> global_reference -> constr -> t -> 
   Proof_type.goal sigma -> t
 
-val re_add_left_list : left_formula list -> t -> t
-
-val change_right : constr -> t -> Proof_type.goal sigma -> t
+val re_add_formula_list : Formula.t list -> t -> t
 
 val find_left : constr -> t -> global_reference
 
-val rev_left : t -> bool
-
-val is_empty_left : t -> bool
-
-val take_left : t -> left_formula * t
-
-val take_right : t -> right_formula
+val take_formula : t -> Formula.t * t
 
 val empty_seq : int -> t