From ba6b5ca0dfc2e49ac2dbb1b49c29a87844a34f76 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 18 Jun 2006 12:17:18 +0000
Subject: [PATCH] - some fixes regarding URIs of equality that now should be
 coherent with the   one of the goal - eliminated the stack overflow issue
 when building the proof

---
 components/tactics/paramodulation/equality.ml |  84 ++--
 .../tactics/paramodulation/equality.mli       |   9 +-
 components/tactics/paramodulation/indexing.ml |  61 ++-
 .../tactics/paramodulation/indexing.mli       |   2 +
 .../tactics/paramodulation/inference.ml       | 102 ++--
 .../tactics/paramodulation/saturation.ml      | 457 ++++--------------
 components/tactics/paramodulation/utils.ml    |  13 -
 components/tactics/paramodulation/utils.mli   |   8 -
 8 files changed, 222 insertions(+), 514 deletions(-)

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 2be5da062..1e9e97ec5 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -433,7 +433,7 @@ let add_subst subst =
 	Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
 ;;
 	
-let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
+let build_proof_step eq lift subst p1 p2 pos l r pred =
   let p1 = Subst.apply_subst_lift lift subst p1 in
   let p2 = Subst.apply_subst_lift lift subst p2 in
   let l  = CicSubstitution.lift lift l in
@@ -453,27 +453,17 @@ let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
   let p =
     match pos with
       | Utils.Left ->
-        mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
+        mk_eq_ind (LibraryObjects.eq_ind_URI ~eq) ty what pred p1 other p2
       | Utils.Right ->
-        mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+        mk_eq_ind (LibraryObjects.eq_ind_r_URI ~eq) ty what pred p1 other p2
   in
-  if sym then
-    let uri,pl,pr = 
-      let eq,_,pl,pr = open_eq body in
-      LibraryObjects.sym_eq_URI ~eq, pl, pr
-    in
-    let l = CicSubstitution.subst other pl in
-    let r = CicSubstitution.subst other pr in
-    mk_sym uri ty l r p
-  else
     p
 ;;
 
 let parametrize_proof p l r ty = 
-  let parameters = CicUtil.metas_of_term p 
-@ CicUtil.metas_of_term l 
-@ CicUtil.metas_of_term r
-in (* ?if they are under a lambda? *)
+  let parameters = 
+    CicUtil.metas_of_term p @ CicUtil.metas_of_term l @ CicUtil.metas_of_term r
+  in (* ?if they are under a lambda? *)
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
@@ -578,7 +568,10 @@ let rec find_deps m i =
     | Step (_,(_,id1,(_,id2),_)) -> 
         let m = find_deps m id1 in
         let m = find_deps m id2 in
-        M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+        (* without the uniq there is a stack overflow doing concatenation *)
+        let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in 
+        let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in
+        M.add i xxx m
 ;;
 
 let topological_sort l = 
@@ -599,13 +592,14 @@ let topological_sort l =
          | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) 
       m
   in
-  let rec aux m = 
+  let rec aux m res = 
       let keys = keys m in
       let ok = split keys m in
       let m = purge ok m in
-      ok @ (if ok = [] then [] else aux m)
+      let res = ok @ res in
+      if ok = [] then res else aux m res
   in
-  aux m
+  aux m []
 ;;
   
 
@@ -642,10 +636,11 @@ let get_duplicate_step_in_wfo l p =
   (* now h is complete *)
   let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
   let proofs = List.filter (fun (_,c) -> c > 1) proofs in
-  topological_sort (List.map (fun (i,_) -> i) proofs)
+  let res = topological_sort (List.map (fun (i,_) -> i) proofs) in
+  res
 ;;
 
-let build_proof_term h lift proof =
+let build_proof_term eq h lift proof =
   let proof_of_id aux id =
     let p,l,r = proof_of_id id in
     try List.assoc id h,l,r with Not_found -> aux p, l, r
@@ -666,7 +661,7 @@ let build_proof_term h lift proof =
            | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let p =   build_proof_step lift subst p1 p2 pos l r pred in
+         let p =   build_proof_step eq lift subst p1 p2 pos l r pred in
 (*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
            if not cond then
              prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
@@ -676,18 +671,17 @@ let build_proof_term h lift proof =
    aux proof
 ;;
 
-let build_goal_proof l initial ty se =
+let build_goal_proof eq l initial ty se =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo l initial in
   let letsno = List.length lets in
   let _,mty,_,_ = open_eq ty in
-  let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l 
-  in
+  let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
   let lets,_,h = 
     List.fold_left
       (fun (acc,n,h) id -> 
         let p,l,r = proof_of_id id in
-        let cic = build_proof_term h n p in
+        let cic = build_proof_term eq h n p in
         let real_cic,instance = 
           parametrize_proof cic l r (CicSubstitution.lift n mty)
         in
@@ -700,7 +694,7 @@ let build_goal_proof l initial ty se =
       | [] -> current_proof,se
       | (rule,pos,id,subst,pred)::tl ->
           let p,l,r = proof_of_id id in
-           let p = build_proof_term h letsno p in
+           let p = build_proof_term eq h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
          let varname = 
            match rule with
@@ -714,13 +708,13 @@ let build_goal_proof l initial ty se =
            | _ -> assert false
          in
            let proof = 
-             build_proof_step letsno subst current_proof p pos l r pred
+             build_proof_step eq letsno subst current_proof p pos l r pred
            in
            let proof,se = aux se proof tl in
            Subst.apply_subst_lift letsno subst proof,
            List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
     in
-    aux se (build_proof_term h letsno initial) l
+    aux se (build_proof_term eq h letsno initial) l
   in
   let n,proof = 
     let initial = proof in
@@ -736,15 +730,20 @@ let build_goal_proof l initial ty se =
    se 
 ;;
 
-let refl_proof ty term = 
-  Cic.Appl 
-    [Cic.MutConstruct 
-       (Utils.eq_URI (), 0, 1, []);
-       ty; term]
+let refl_proof eq_uri ty term = 
+  Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term]
 ;;
 
 let metas_of_proof p =
-  let p = build_proof_term [] 0 p in
+  let eq = 
+    match LibraryObjects.eq_URI () with
+    | Some u -> u 
+    | None -> 
+        raise 
+          (ProofEngineTypes.Fail 
+            (lazy "No default equality defined when calling metas_of_proof"))
+  in
+  let p = build_proof_term eq [] 0 p in
   Utils.metas_of_term p
 ;;
 
@@ -915,17 +914,16 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
-  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] 
+    when LibraryObjects.is_eq_URI uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = Utils.eq_URI () in
-  let iseq uri = UriManager.eq uri eq_uri in
   match term with
-  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] 
+    when LibraryObjects.is_eq_URI uri ->
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = Utils.compute_equality_weight stat in
@@ -948,13 +946,13 @@ let is_identity (_, context, ugraph) eq =
 ;;
 
 
-let term_of_equality equality =
+let term_of_equality eq_uri equality =
   let _, _, (ty, left, right, _), menv, _= open_equality equality in
   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (eq_uri, 0, []); ty; left; right])
   in
   snd (
     List.fold_right
diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index cd60c5408..237045bec 100644
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -61,11 +61,12 @@ val string_of_proof :
   ?names:(Cic.name option)list -> proof -> goal_proof -> string
 (* given a proof and a list of meta indexes we are interested in the
  * instantiation gives back the cic proof and the list of instantiations *)  
-(* build_goal_proof [goal_proof] [initial_proof] [ty] 
+(* build_goal_proof [eq_URI] [goal_proof] [initial_proof] [ty] 
  *  [ty] is the type of the goal *)
 val build_goal_proof: 
-  goal_proof -> proof -> Cic.term-> int list -> Cic.term * Cic.term list
-val refl_proof: Cic.term -> Cic.term -> Cic.term 
+  UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> 
+    Cic.term * Cic.term list
+val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
 val metas_of_proof: proof -> int list
@@ -82,7 +83,7 @@ val equality_of_term: Cic.term -> Cic.term -> equality
 (**
    Re-builds the term corresponding to this equality
 *)
-val term_of_equality: equality -> Cic.term
+val term_of_equality: UriManager.uri -> equality -> Cic.term
 val term_is_equality: Cic.term -> bool
 
 (** tests a sort of alpha-convertibility between the two terms, but on the
diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 925aab6e0..7aafcbcd6 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -61,7 +61,7 @@ type retrieval_mode = Matching | Unification;;
 let string_of_res ?env =
   function
       None -> "None"
-    | Some (t, s, m, u, ((p,e), eq_URI)) ->
+    | Some (t, s, m, u, (p,e)) ->
         Printf.sprintf "Some: (%s, %s, %s)" 
           (Utils.string_of_pos p)
           (Equality.string_of_equality ?env e)
@@ -122,7 +122,7 @@ let check_for_duplicates metas msg =
 
 let check_res res msg =
   match res with
-      Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
+      Some (t, subst, menv, ug, eq_found) ->
         let eqs = Equality.string_of_equality (snd eq_found) in
         check_disjoint_invariant subst menv msg;
         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
@@ -252,22 +252,21 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                                 ~metasenv context termty ty ugraph)) then (
           find_matches metasenv context ugraph lift_amount term termty tl
         ) else
-          let do_match c eq_URI =
+          let do_match c =
             let subst', metasenv', ugraph' =
               Inference.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
-            Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
-                  (candidate, eq_URI))
+            Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
           in
-          let c, other, eq_URI =
-            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
-            else right, left, Utils.eq_ind_r_URI ()
+          let c, other =
+            if pos = Utils.Left then left, right
+            else right, left
           in
           if o <> U.Incomparable then
             let res =
               try
-                do_match c eq_URI
+                do_match c 
               with Inference.MatchingFailure ->
                 find_matches metasenv context ugraph lift_amount term termty tl
             in
@@ -275,7 +274,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
               res
           else
             let res =
-              try do_match c eq_URI
+              try do_match c 
               with Inference.MatchingFailure -> None
             in
             if Utils.debug_res then ignore (check_res res "find2");
@@ -316,19 +315,19 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
     | candidate::tl ->
         let pos, equality = candidate in 
         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
-        let do_match c eq_URI =
+        let do_match c =
           let subst', metasenv', ugraph' =
             unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
           in
-          (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
+          (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
         in
-        let c, other, eq_URI =
-          if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
-          else right, left, Utils.eq_ind_r_URI ()
+        let c, other =
+          if pos = Utils.Left then left, right
+          else right, left
         in
         if o <> U.Incomparable then
           try
-            let res = do_match c eq_URI in
+            let res = do_match c in
             res::(find_all_matches ~unif_fun metasenv context ugraph
                     lift_amount term termty tl)
           with
@@ -339,7 +338,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                 lift_amount term termty tl
         else
           try
-            let res = do_match c eq_URI in
+            let res = do_match c in
             match res with
             | _, s, _, _, _ ->
                 let c' = apply_subst s c
@@ -397,7 +396,7 @@ let subsumption_aux use_unification env table target =
   in
   let rec ok what leftorright = function
     | [] -> None
-    | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+    | (_, subst, menv, ug, (pos,equation))::tl ->
         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
         try
           let other = if pos = Utils.Left then r else l in
@@ -537,7 +536,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality ?from newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table sign target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -559,7 +558,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let metasenv' = (* metasenv @ *) metas in
   let maxmeta = ref newmeta in
   
-  let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
+  let build_newtarget is_left (t, subst, menv, ug, eq_found) =
     
     if Utils.debug_metas then
       begin
@@ -583,8 +582,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
       let name = C.Name "x" in
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
-          C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
-                  S.lift 1 eq_ty; l; r]
+          C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
@@ -693,7 +691,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality ?from newmeta env table sign newtarget
+            demodulation_equality ?from eq_uri newmeta env table sign newtarget
     | None ->
         let res = demodulation_aux metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
@@ -704,7 +702,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality ?from newmeta env table sign newtarget
+                   demodulation_equality ?from eq_uri newmeta env table sign newtarget
           | None ->
               newmeta, target
   in
@@ -851,8 +849,7 @@ let rec betaexpand_term
    index: its updated value is also returned
 *)
 let superposition_right 
-  ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target 
-=
+  ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -883,7 +880,7 @@ let superposition_right
         in
         (res left right), (res right left)
   in
-  let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
+  let build_new ordering (bo, s, m, ug, eq_found) =
     if Utils.debug_metas then 
       ignore (check_target context (snd eq_found) "buildnew1" );
     
@@ -901,8 +898,7 @@ let superposition_right
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
-                S.lift 1 eq_ty; l; r]
+        C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
       bo',
         Equality.Step 
@@ -949,7 +945,7 @@ let rec demodulation_theorem newmeta env table theorem =
   let term, termty, metas = theorem in
   let metasenv' = metas in
   
-  let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
+  let build_newtheorem (t, subst, menv, ug, eq_found) =
     let pos, equality = eq_found in
     let (_, proof', (ty, what, other, _), menv',id) = 
       Equality.open_equality equality in
@@ -1028,7 +1024,7 @@ let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
  * expansion builds a new goal *)
 let build_newgoal context goal posu rule expansion =
   let goalproof,_,_,_,_,_ = open_goal goal in
-  let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
+  let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
   let pos, equality = eq_found in
   let (_, proof', (ty, what, other, _), menv',id) = 
     Equality.open_equality equality in
@@ -1062,9 +1058,6 @@ let superposition_left (metasenv, context, ugraph) table goal =
   if c = Utils.Incomparable then
     let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
     let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
-    prerr_endline "ZZZ";
-    prerr_endline (string_of_int (List.length expansionsl));
-    prerr_endline (string_of_int (List.length expansionsr));
     List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
     @
     List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index a446747e5..7caaa78f4 100644
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -59,6 +59,7 @@ val superposition_left :
 
 val superposition_right :
   ?subterms_only:bool ->
+    UriManager.uri ->
   int ->
   'a * Cic.context * CicUniv.universe_graph ->
   Index.t ->
@@ -67,6 +68,7 @@ val superposition_right :
 
 val demodulation_equality :
   ?from:string -> 
+  UriManager.uri ->
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 6004de44c..e2f85fa2b 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -211,7 +211,6 @@ let find_equalities context proof =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let eq_uri = Utils.eq_URI () in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -234,7 +233,8 @@ let find_equalities context proof =
               in (
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                    when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
+                    when (LibraryObjects.is_eq_URI uri) && 
+                         (ok_types ty newmetas) ->
                     debug_print
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
@@ -247,7 +247,7 @@ let find_equalities context proof =
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-              when UriManager.eq uri eq_uri ->
+              when LibraryObjects.is_eq_URI uri ->
               let ty = S.lift index ty in
               let t1 = S.lift index t1 in
               let t2 = S.lift index t2 in
@@ -315,43 +315,39 @@ let equations_blacklist =
 *)
 let equations_blacklist = UriManager.UriSet.empty;;
 
+let tty_of_u u = 
+  let _ = <:start<tty_of_u>> in
+  let t = CicUtil.term_of_uri u in
+  let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+  let _ = <:stop<tty_of_u>> in
+  t, ty
+;;
+
+let utty_of_u u =
+  let t,ty = tty_of_u u in
+  u, t, ty
+;;
 
 let find_library_equalities dbd context status maxmeta = 
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let blacklist =
-    List.fold_left
-      (fun s u -> UriManager.UriSet.add u s)
-      equations_blacklist
-      [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
-       eq_ind_r_URI ()]
-  in
+  let _ = <:start<equations_for_goal>> in
+  let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
+  let _ = <:stop<equations_for_goal>> in
   let candidates =
     List.fold_left
       (fun l uri ->
-         if UriManager.UriSet.mem uri blacklist then
+        if LibraryObjects.is_eq_refl_URI uri ||
+           LibraryObjects.is_sym_eq_URI uri ||
+           LibraryObjects.is_trans_eq_URI uri ||
+           LibraryObjects.is_eq_ind_URI uri ||
+           LibraryObjects.is_eq_ind_r_URI uri 
+         then 
            l
          else
-           let t = CicUtil.term_of_uri uri in
-           let ty, _ =
-             CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
-           in
-           (uri, t, ty)::l)
-      []
-      (let t1 = Unix.gettimeofday () in
-       let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
-       let t2 = Unix.gettimeofday () in
-       (debug_print
-          (lazy
-             (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
-                (t2 -. t1))));
-       eqs)
-  in
-  let eq_uri1 = eq_XURI ()
-  and eq_uri2 = Utils.eq_URI () in
-  let iseq uri =
-    (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
+           (utty_of_u uri)::l)
+      [] eqs
   in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -386,7 +382,9 @@ let find_library_equalities dbd context status maxmeta =
               in (
                   match head with
                     | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                        when (iseq uri) && (ok_types ty newmetas) ->
+                        when (LibraryObjects.is_eq_URI uri ||
+                              LibraryObjects.is_eq_refl_URI uri) && 
+                             (ok_types ty newmetas) ->
                     debug_print
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
@@ -399,7 +397,10 @@ let find_library_equalities dbd context status maxmeta =
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-              when iseq uri && not (has_vars termty) ->
+              when 
+                (LibraryObjects.is_eq_URI uri || 
+                 LibraryObjects.is_eq_refl_URI uri) && 
+                not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
@@ -439,36 +440,33 @@ let find_library_theorems dbd env status equalities_uris =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let blacklist =
-    let refl_equal =
-      UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
-    let s =
-      UriManager.UriSet.remove refl_equal
-        (UriManager.UriSet.union equalities_uris equations_blacklist)
-    in
-    List.fold_left
-      (fun s u -> UriManager.UriSet.add u s)
-      s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
-         eq_ind_r_URI ()]
-  in
-  let metasenv, context, ugraph = env in
   let candidates =
     List.fold_left
       (fun l uri ->
-         if UriManager.UriSet.mem uri blacklist then l
+        if LibraryObjects.is_sym_eq_URI uri ||
+           LibraryObjects.is_trans_eq_URI uri ||
+           LibraryObjects.is_eq_ind_URI uri ||
+           LibraryObjects.is_eq_ind_r_URI uri 
+         then l
          else
-           let t = CicUtil.term_of_uri uri in
-           let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
-           (t, ty, [])::l)
+           (let t,ty = tty_of_u uri in t, ty, [] )::l)
       [] (MetadataQuery.signature_of_goal ~dbd status)
   in
   let refl_equal =
-    let u = eq_XURI () in
-    let t = CicUtil.term_of_uri u in
+    let eq = 
+      match LibraryObjects.eq_URI () with
+      | Some u -> u
+      | None -> 
+          raise 
+            (ProofEngineTypes.Fail 
+              (lazy "No default eq defined when running find_library_theorems"))
+    in
+    let t = CicUtil.term_of_uri (LibraryObjects.eq_refl_URI ~eq) in
     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
     (t, ty, [])
   in
-  refl_equal::candidates
+  let res = refl_equal::candidates in
+  res
 ;;
 
 
diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index fe63c7d66..b50e0a49f 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -336,7 +336,7 @@ let prune_passive howmany (active, _) passive =
 
 
 (** inference of new equalities between current and some in active *)
-let infer env current (active_list, active_table) =
+let infer eq_uri env current (active_list, active_table) =
   let (_,c,_) = env in 
   if Utils.debug_metas then
     (ignore(Indexing.check_target c current "infer1");
@@ -347,7 +347,7 @@ let infer env current (active_list, active_table) =
       let active_table =  Indexing.index active_table copy_of_current in
       let _ = <:start<current contro active>> in
       let maxm, res =
-        Indexing.superposition_right !maxmeta env active_table current 
+        Indexing.superposition_right eq_uri !maxmeta env active_table current 
       in
       let _ = <:stop<current contro active>> in
       if Utils.debug_metas then
@@ -359,7 +359,8 @@ let infer env current (active_list, active_table) =
         | [] -> []
         | equality::tl ->
             let maxm, res =
-              Indexing.superposition_right ~subterms_only:true !maxmeta env table equality 
+              Indexing.superposition_right 
+                ~subterms_only:true eq_uri !maxmeta env table equality 
             in
               maxmeta := maxm;
               if Utils.debug_metas then
@@ -431,7 +432,9 @@ let check_for_deep_subsumption env active_table eq =
 (* buttare via sign *)
 
 (** simplifies current using active and passive *)
-let forward_simplify env (sign,current) ?passive (active_list, active_table) =
+let forward_simplify 
+  eq_uri env (sign,current) ?passive (active_list, active_table) 
+=
   let _, context, _ = env in
   let passive_table =
     match passive with
@@ -440,7 +443,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
   in
   let demodulate table current = 
     let newmeta, newcurrent =
-      Indexing.demodulation_equality !maxmeta env table sign current in
+      Indexing.demodulation_equality eq_uri !maxmeta env table sign current in
     maxmeta := newmeta;
     if Equality.is_identity env newcurrent then
       None
@@ -506,7 +509,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
 ;;
 
 (** simplifies new using active and passive *)
-let forward_simplify_new env new_pos ?passive active =
+let forward_simplify_new eq_uri env new_pos ?passive active =
   if Utils.debug_metas then
     begin
       let m,c,u = env in
@@ -522,7 +525,8 @@ let forward_simplify_new env new_pos ?passive active =
   in
   let demodulate sign table target =
     let newmeta, newtarget =
-      Indexing.demodulation_equality !maxmeta env table sign target in
+      Indexing.demodulation_equality eq_uri !maxmeta env table sign target 
+    in
     maxmeta := newmeta;
     newtarget
   in
@@ -602,7 +606,7 @@ let simplify_goals env goals ?passive active =
 
 
 (** simplifies active usign new *)
-let backward_simplify_active env new_pos new_table min_weight active =
+let backward_simplify_active eq_uri env new_pos new_table min_weight active =
   let active_list, active_table = active in
   let active_list, newa, pruned = 
     List.fold_right
@@ -611,7 +615,10 @@ let backward_simplify_active env new_pos new_table min_weight active =
          if ew < min_weight then
            equality::res, newn,pruned
          else
-           match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with
+           match 
+             forward_simplify 
+               eq_uri env (Utils.Positive, equality) (new_pos, new_table) 
+           with
            | None -> res, newn, id::pruned
            | Some e ->
                if Equality.compare equality e = 0 then
@@ -650,14 +657,16 @@ let backward_simplify_active env new_pos new_table min_weight active =
 
 
 (** simplifies passive using new *)
-let backward_simplify_passive env new_pos new_table min_weight passive =
+let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
   let (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
     let ew, _, _, _ , _ = Equality.open_equality equality in
     if ew < min_weight then
       equality::resl, ress, newn
     else
-      match forward_simplify env (sign, equality) (new_pos, new_table) with
+      match 
+        forward_simplify eq_uri env (sign, equality) (new_pos, new_table) 
+      with
       | None -> resl, EqualitySet.remove equality ress, newn
       | Some e ->
           if equality = e then
@@ -685,7 +694,7 @@ let build_table equations =
 ;;
   
 
-let backward_simplify env new' ?passive active =
+let backward_simplify eq_uri env new' ?passive active =
   let new_pos, new_table, min_weight = build_table new' in
 (*
     List.fold_left
@@ -696,7 +705,8 @@ let backward_simplify env new' ?passive active =
   in
 *)
   let active, newa, pruned =
-    backward_simplify_active env new_pos new_table min_weight active in
+    backward_simplify_active eq_uri env new_pos new_table min_weight active 
+  in
   match passive with
   | None ->
       active, (make_passive []), newa, None, pruned
@@ -708,7 +718,7 @@ let backward_simplify env new' ?passive active =
       active, passive, newa, newp *)
 ;;
 
-let close env new' given =
+let close eq_uri env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
@@ -718,7 +728,7 @@ let close env new' given =
   in
   List.fold_left
     (fun p c ->
-       let pos = infer env c (new_pos,new_table) in
+       let pos = infer eq_uri env c (new_pos,new_table) in
          pos@p)
     [] given 
 ;;
@@ -734,7 +744,7 @@ let is_commutative_law eq =
       | _ -> false
 ;;
 
-let prova env new' active = 
+let prova eq_uri env new' active = 
   let given = List.filter is_commutative_law (fst active) in
   let _ =
     debug_print
@@ -744,7 +754,7 @@ let prova env new' active =
                (List.map
                   (fun e -> Equality.string_of_equality ~env e)
                    given)))) in
-    close env new' given
+    close eq_uri env new' given
 ;;
 
 (* returns an estimation of how many equalities in passive can be activated
@@ -827,19 +837,19 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
 ;;
 
 
-let rec simpl env e others others_simpl =
+let rec simpl eq_uri env e others others_simpl =
   let active = others @ others_simpl in
   let tbl =
     List.fold_left
       (fun t e -> Indexing.index t e)
       Indexing.empty active
   in
-  let res = forward_simplify env (Positive,e) (active, tbl) in
+  let res = forward_simplify eq_uri env (Positive,e) (active, tbl) in
     match others with
       | hd::tl -> (
           match res with
-            | None -> simpl env hd tl others_simpl
-            | Some e -> simpl env hd tl (e::others_simpl)
+            | None -> simpl eq_uri env hd tl others_simpl
+            | Some e -> simpl eq_uri env hd tl (e::others_simpl)
         )
       | [] -> (
           match res with
@@ -848,7 +858,7 @@ let rec simpl env e others others_simpl =
         )
 ;;
 
-let simplify_equalities env equalities =
+let simplify_equalities eq_uri env equalities =
   debug_print
     (lazy 
        (Printf.sprintf "equalities:\n%s\n"
@@ -859,7 +869,7 @@ let simplify_equalities env equalities =
     | [] -> []
     | hd::tl ->
         let res =
-          List.rev (simpl env hd tl [])
+          List.rev (simpl eq_uri env hd tl [])
         in
           debug_print
             (lazy
@@ -888,7 +898,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 *)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
-    when UriManager.eq uri (Utils.eq_URI ()) ->
+    when LibraryObjects.is_eq_URI uri ->
       (let goal_equation = 
          Equality.mk_equality
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
@@ -912,303 +922,19 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
   | _ -> None
 ;;
 
-let counter = ref 0
-
-(** given-clause algorithm with full reduction strategy *)
-let rec given_clause_fullred dbd env goals theorems ~passive active =
-  let goals = simplify_goals env goals ~passive active in 
-  let _,context,_ = env in
-  let ok, (goals:
-    (Equality.goal_proof * Cic.metasenv * Cic.term) list * 
-    (Equality.goal_proof * Cic.metasenv * Cic.term) list) = activate_goal 
-    
-    (goals: 
-  (Equality.goal_proof * Cic.metasenv * Cic.term) list * 
-    (Equality.goal_proof * Cic.metasenv * Cic.term) list)
-  in
-(*   let theorems = simplify_theorems env theorems ~passive active in *)
-  if ok then
-    let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in 
-    let _, _, t = List.hd (fst goals) in
-    let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in
-(*     let _ = *)
-(*       debug_print *)
-(*         (lazy *)
-(*            (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *)
-(*               (print_goals (fst goals)) (print_goals (snd goals)))); *)
-(*       let current = List.hd (fst goals) in *)
-(*       let p, _, t = List.hd (snd current) in *)
-(*       debug_print *)
-(*         (lazy *)
-(*            (Printf.sprintf "goal activated:\n%s\n%s\n" *)
-(*               (CicPp.ppterm t) (string_of_proof p))); *)
-(*     in *)
-    let ok, proof =
-      (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
-      let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
-      match fst goals with
-        | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ 
-            when left = right && iseq uri -> 
-            let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
-            true, Some (goalproof, reflproof, 0, Subst.empty_subst,m)
-        | goal::_ ->
-            (match check_if_goal_is_subsumed env (snd active) goal with
-            | None -> false,None
-            | Some p ->
-                prerr_endline "Proof found by subsumption!";
-                true, Some p)
-        | _ -> false, None
-    in 
-    if ok then
-      ( prerr_endline "esco qui";
-        (*
-        let s = Printf.sprintf "actives:\n%s\n"
-          (String.concat "\n"
-             ((List.map
-                 (fun (s, e) -> (string_of_sign s) ^ " " ^
-                    (string_of_equality ~env e))
-                 (fst active)))) in
-        let sp = Printf.sprintf "passives:\n%s\n"
-          (String.concat "\n"
-             (List.map
-                (string_of_equality ~env)
-                (let x,y,_ = passive in (fst x)@(fst y)))) in
-          prerr_endline s;
-          prerr_endline sp; *)
-        match proof with 
-        | None -> assert false 
-        | Some p ->  ParamodulationSuccess p)
-    else
-      given_clause_fullred_aux dbd env goals theorems passive active
-  else
-(*     let ok', theorems = activate_theorem theorems in *)
-(*     if ok' then *)
-(*       let ok, goals = apply_theorem_to_goals env theorems active goals in *)
-(*       if ok then *)
-(*         let proof = *)
-(*           match (fst goals) with *)
-(*           | (_, [proof, _, _])::_ -> Some proof *)
-(*           | _ -> assert false *)
-(*         in *)
-(*         ParamodulationSuccess (proof, env) *)
-(*       else *)
-(*         given_clause_fullred_aux env goals theorems passive active *)
-(*     else *)
-      if (passive_is_empty passive) then ParamodulationFailure ""
-      else given_clause_fullred_aux dbd env goals theorems passive active
-    
-and given_clause_fullred_aux dbd env goals theorems passive active =
-  prerr_endline (string_of_int !counter ^ 
-                 " MAXMETA: " ^ string_of_int !maxmeta ^ 
-                 " #ACTIVES: " ^ string_of_int (size_of_active active) ^
-                 " #PASSIVES: " ^ string_of_int (size_of_passive passive));
-  incr counter;
-(*
-    if !counter mod 10 = 0 then
-    begin
-      let size = HExtlib.estimate_size (passive,active) in
-      let sizep = HExtlib.estimate_size (passive) in
-      let sizea = HExtlib.estimate_size (active) in
-      let (l1,s1),(l2,s2), t = passive in 
-      let sizetbl = HExtlib.estimate_size t in
-      let sizel = HExtlib.estimate_size (l1,l2) in
-      let sizes = HExtlib.estimate_size (s1,s2) in
-
-      prerr_endline ("SIZE: " ^ string_of_int size);        
-      prerr_endline ("SIZE P: " ^ string_of_int sizep);        
-      prerr_endline ("SIZE A: " ^ string_of_int sizea);        
-      prerr_endline ("SIZE TBL: " ^ string_of_int sizetbl ^ 
-                       " SIZE L: " ^ string_of_int sizel ^ 
-                       " SIZE S:" ^ string_of_int sizes);
-    end;*)
-(*
-  if (size_of_active active) mod 50 = 0 then
-    (let s = Printf.sprintf "actives:\n%s\n"
-      (String.concat "\n"
-         ((List.map
-             (fun (s, e) -> (string_of_sign s) ^ " " ^
-                (string_of_equality ~env e))
-             (fst active)))) in
-     let sp = Printf.sprintf "passives:\n%s\n"
-      (String.concat "\n"
-         (List.map
-             (string_of_equality ~env)
-             (let x,y,_ = passive in (fst x)@(fst y)))) in
-      prerr_endline s;
-      prerr_endline sp); *)
-  let time1 = Unix.gettimeofday () in
-  let (_,context,_) = env in
-  let selection_estimate = get_selection_estimate () in
-  let kept = size_of_passive passive in
-  let passive =
-    if !time_limit = 0. || !processed_clauses = 0 then
-      passive
-    else if !elapsed_time > !time_limit then (
-      debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
-                           !time_limit !elapsed_time));
-      make_passive [] 
-    ) else if kept > selection_estimate then (
-      debug_print
-        (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
-                                 "(kept: %d, selection_estimate: %d)\n")
-                 kept selection_estimate));
-      prune_passive selection_estimate active passive
-    ) else
-      passive
-  in
-
-  let time2 = Unix.gettimeofday () in
-  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
-  
-  kept_clauses := (size_of_passive passive) + (size_of_active active);
-  match passive_is_empty passive with
-  | true -> ParamodulationFailure ""
-      (* given_clause_fullred dbd env goals theorems passive active  *)     
-  | false ->
-      let current, passive = select env goals passive in
-      prerr_endline 
-        ("Selected = " ^ Equality.string_of_equality ~env current);
-(* ^ 
-           (let w,p,(t,l,r,o),m = current in
-           " size w: " ^ string_of_int (HExtlib.estimate_size w)^
-           " size p: " ^ string_of_int (HExtlib.estimate_size p)^
-           " size t: " ^ string_of_int (HExtlib.estimate_size t)^
-           " size l: " ^ string_of_int (HExtlib.estimate_size l)^
-           " size r: " ^ string_of_int (HExtlib.estimate_size r)^
-           " size o: " ^ string_of_int (HExtlib.estimate_size o)^
-           " size m: " ^ string_of_int (HExtlib.estimate_size m)^
-           " size m-c: " ^ string_of_int 
-             (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *)
-      let time1 = Unix.gettimeofday () in
-      let res = forward_simplify env (Positive, current) ~passive active in
-      let time2 = Unix.gettimeofday () in
-      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
-      match res with
-      | None ->
-          (* weight_age_counter := !weight_age_counter + 1; *)
-          given_clause_fullred dbd env goals theorems passive active
-      | Some current ->
-(*          prerr_endline (Printf.sprintf "selected simpl: %s"
-                               (Equality.string_of_equality ~env current));*)
-          let t1 = Unix.gettimeofday () in
-          let new' = infer env current active in
-          let _ =
-            debug_print
-              (lazy
-                 (Printf.sprintf "new' (senza semplificare):\n%s\n"
-                    (String.concat "\n"
-                       (List.map
-                          (fun e -> "Positive " ^
-                             (Equality.string_of_equality ~env e)) new'))))
-          in
-          let t2 = Unix.gettimeofday () in
-            infer_time := !infer_time +. (t2 -. t1);
-            let active =
-              if Equality.is_identity env current then active
-              else
-                let al, tbl = active in
-                  al @ [current], Indexing.index tbl current
-            in
-            let rec simplify new' active passive =
-              let t1 = Unix.gettimeofday () in
-              let new' = forward_simplify_new env new'~passive active in
-              let t2 = Unix.gettimeofday () in
-              forward_simpl_new_time :=
-                !forward_simpl_new_time +. (t2 -. t1);
-              let t1 = Unix.gettimeofday () in
-              let active, passive, newa, retained, pruned =
-                backward_simplify env new' ~passive  active in
-              let passive = 
-                List.fold_left filter_dependent passive pruned in
-              let t2 = Unix.gettimeofday () in
-                backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
-              match newa, retained with
-              | None, None -> active, passive, new'
-              | Some p, None
-              | None, Some p ->
-                  if Utils.debug_metas then
-                    begin
-                      List.iter 
-                        (fun x->Indexing.check_target context x "simplify1")
-                        p;
-                    end;
-                  simplify (new' @ p) active passive
-              | Some p, Some rp ->
-                  simplify (new' @ p @ rp) active passive
-            in
-            let active, passive, new' = simplify new' active passive in
-            let goals = 
-              let a,b,_ = build_table new' in
-              simplify_goals env goals ~passive (a,b)
-            in
-              
-(* pessima prova 
-            let new1 = prova env new' active in
-            let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
-            let _ =
-              match new1 with
-              | neg, pos ->
-                  debug_print
-                    (lazy
-                       (Printf.sprintf "new1:\n%s\n"
-                          (String.concat "\n"
-                             ((List.map
-                                 (fun e -> "Negative " ^
-                                    (string_of_equality ~env e)) neg) @
-                                (List.map
-                                   (fun e -> "Positive " ^
-                                      (string_of_equality ~env e)) pos)))))
-            in
-end prova *)
-            let k = size_of_passive passive in
-            if k < (kept - 1) then
-              processed_clauses := !processed_clauses + (kept - 1 - k);
-            
-            let _ =
-              debug_print
-                (lazy
-                   (Printf.sprintf "active:\n%s\n"
-                      (String.concat "\n"
-                         ((List.map
-                             (fun e -> (Equality.string_of_equality ~env e))
-                             (fst active))))))
-            in
-            let _ =
-              debug_print
-                (lazy
-                   (Printf.sprintf "new':\n%s\n"
-                      (String.concat "\n"
-                         ((List.map
-                             (fun e -> "Negative " ^
-                                (Equality.string_of_equality ~env e)) new')))))
-            in
-            let passive = add_to_passive passive new' in
-              given_clause_fullred dbd env goals theorems passive active
-;;
-
-(*
-let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred"
-
-let given_clause_fullred dbd env goals theorems passive active =
-  profiler0.HExtlib.profile 
-    (given_clause_fullred dbd env goals theorems passive) active
-*)
-
-let iseq uri = UriManager.eq uri (Utils.eq_URI ());;
-
 let check_if_goal_is_identity env = function
   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
-    when left = right && iseq uri ->
-      let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+    when left = right && LibraryObjects.is_eq_URI uri ->
+      let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       Some (goalproof, reflproof, 0, Subst.empty_subst,m)
   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
-    when iseq uri ->
+    when LibraryObjects.is_eq_URI uri ->
     (let _,context,_ = env in
     try 
      let s,m,_ = 
        Inference.unification m m context left right CicUniv.empty_ugraph 
      in
-      let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+      let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       let m = Subst.apply_subst_metasenv s m in
       Some (goalproof, reflproof, 0, s,m)
     with _ -> None)
@@ -1270,7 +996,13 @@ let infer_goal_set env active goals =
        -> 
         let selected = hd in
         let passive_goals = tl in
-        let new' = Indexing.superposition_left env (snd active) selected in
+        let _,_,ty = selected in 
+        let new' = 
+          if CicUtil.is_meta_closed ty then
+            []
+          else
+            Indexing.superposition_left env (snd active) selected 
+        in
         selected::active_goals, passive_goals @ new'
     | _::tl -> aux tl
   in 
@@ -1280,16 +1012,10 @@ let infer_goal_set env active goals =
 let infer_goal_set_with_current env current goals = 
   let active_goals, passive_goals = goals in
   let _,table,_ = build_table [current] in
-  let _,_,_,_,id = Equality.open_equality current in
   active_goals,
   List.fold_left 
     (fun acc g ->
       let new' = Indexing.superposition_left env table g in
-      if id = 2 then
-        begin
-	 prerr_endline "XXXXXXX";
-	 List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ;
-	end;
       acc @ new')
     passive_goals active_goals
 ;;
@@ -1302,7 +1028,7 @@ let size_of_goal_set_p (_,l) = List.length l;;
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
 (* here goals is a set of goals in OR *)
 let given_clause 
-  ((_,context,_) as env) goals theorems passive active max_iterations max_time
+  eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
 = 
   let names = names_of_context context in
   let initial_time = Unix.gettimeofday () in
@@ -1356,8 +1082,6 @@ let given_clause
             ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
-              let goals = infer_goal_set env active goals in
-              let goals = infer_goal_set env active goals in
               let goals = infer_goal_set env active goals in
               let current, passive = select env goals passive in
               let _,_,goaltype = List.hd (fst goals) in                
@@ -1367,14 +1091,14 @@ let given_clause
                 (Equality.string_of_equality ~env current));
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
-                forward_simplify env (Positive, current) (*~passive*) active 
+                forward_simplify eq_uri env (Positive, current) active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
                   prerr_endline "infer";
-                  let new' = infer env current active in
+                  let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
                   let active = 
@@ -1384,9 +1108,11 @@ let given_clause
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
                   prerr_endline "fwd/back simpl";
                   let rec simplify new' active passive =
-                    let new' = forward_simplify_new env new' ~passive active in
+                    let new' = 
+                      forward_simplify_new eq_uri env new' ~passive active 
+                    in
                     let active, passive, newa, retained, pruned =
-                      backward_simplify env new' ~passive  active 
+                      backward_simplify eq_uri env new' ~passive  active 
                     in
                     let passive = 
                       List.fold_left filter_dependent passive pruned 
@@ -1398,21 +1124,13 @@ let given_clause
                     | Some p, Some rp -> simplify (new' @ p @ rp) active passive
                   in
                   let active, passive, new' = simplify new' active passive in
-                  if iterno = 36 || iterno = 654 then
-                   begin 
-                     prerr_endline "...................";
-                     List.iter 
-                       (fun x -> prerr_endline (Equality.string_of_equality 
-~env:env x)) new';
-                     prerr_endline "FINE...................";
-                   end;
                   prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
                     let _ = <:start<simplify_goal_set new>> in
-                    <:stop<simplify_goal_set new
-                    simplify_goal_set env goals passive (a,b)
-                    >>
+                    let rc = simplify_goal_set env goals passive (a,b) in
+                    let _ = <:stop<simplify_goal_set new>> in
+                    rc
                   in
                   let passive = add_to_passive passive new' in
                   step goals theorems passive active (iterno+1)
@@ -1421,20 +1139,20 @@ let given_clause
     step goals theorems passive active 1
 ;;
 
-let rec saturate_equations env goal accept_fun passive active =
+let rec saturate_equations eq_uri env goal accept_fun passive active =
   elapsed_time := Unix.gettimeofday () -. !start_time;
   if !elapsed_time > !time_limit then
     (active, passive)
   else
     let current, passive = select env ([goal],[]) passive in
-    let res = forward_simplify env (Positive, current) ~passive active in
+    let res = forward_simplify eq_uri env (Positive, current) ~passive active in
     match res with
     | None ->
-        saturate_equations env goal accept_fun passive active
+        saturate_equations eq_uri env goal accept_fun passive active
     | Some current ->
         debug_print (lazy (Printf.sprintf "selected: %s"
                              (Equality.string_of_equality ~env current)));
-        let new' = infer env current active in
+        let new' = infer eq_uri env current active in
         let active =
           if Equality.is_identity env current then active
           else
@@ -1442,9 +1160,9 @@ let rec saturate_equations env goal accept_fun passive active =
             al @ [current], Indexing.index tbl current
         in
         let rec simplify new' active passive =
-          let new' = forward_simplify_new env new' ~passive active in
+          let new' = forward_simplify_new eq_uri env new' ~passive active in
           let active, passive, newa, retained, pruned =
-            backward_simplify env new' ~passive active in
+            backward_simplify eq_uri env new' ~passive active in
           let passive = 
             List.fold_left filter_dependent passive pruned in
           match newa, retained with
@@ -1474,7 +1192,7 @@ let rec saturate_equations env goal accept_fun passive active =
         in
         let new' = List.filter accept_fun new' in
         let passive = add_to_passive passive new' in
-        saturate_equations env goal accept_fun passive active
+        saturate_equations eq_uri env goal accept_fun passive active
 ;;
   
 let main dbd full term metasenv ugraph = ()
@@ -1664,18 +1382,24 @@ let reset_refs () =
   Equality.reset ();
 ;;
 
+let eq_of_goal = function
+  | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
+      uri
+  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
 let saturate 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
   reset_refs ();
   Indexing.init_index ();
-  counter := 0;
   maxdepth := depth;
   maxwidth := width;
 (*  CicUnification.unif_ty := false;*)
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
   let names = names_of_context context in
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
@@ -1689,7 +1413,9 @@ let saturate
     let library_equalities = List.map snd library_equalities in
     let t2 = Unix.gettimeofday () in
     maxmeta := maxm+2;
-    let equalities = simplify_equalities env (equalities@library_equalities) in 
+    let equalities = 
+      simplify_equalities eq_uri env (equalities@library_equalities) 
+    in 
     debug_print
       (lazy
          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
@@ -1700,10 +1426,7 @@ let saturate
         let context_hyp = find_context_hypotheses env eq_indexes in
         context_hyp @ thms, []
       else
-        let refl_equal =
-          let us = UriManager.string_of_uri (Utils.eq_URI ()) in
-          UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
-        in
+        let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
         let t = CicUtil.term_of_uri refl_equal in
         let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
         [(t, ty, [])], []
@@ -1735,8 +1458,9 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
-      given_clause env goals theorems passive active max_iterations max_time 
+      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      given_clause 
+        eq_uri env goals theorems passive active max_iterations max_time 
     in
     let finish = Unix.gettimeofday () in
     (res, finish -. start)
@@ -1760,7 +1484,8 @@ let saturate
       in
       let goal_proof, side_effects_t = 
         let initial = Equality.add_subst subsumption_subst newproof in
-        Equality.build_goal_proof goalproof initial type_of_goal side_effects
+        Equality.build_goal_proof 
+          eq_uri goalproof initial type_of_goal side_effects
       in
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
@@ -1871,6 +1596,7 @@ let retrieve_and_print dbd term metasenv ugraph =
   let goal' = List.nth goals 0 in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in
@@ -1901,7 +1627,7 @@ let retrieve_and_print dbd term metasenv ugraph =
         (fun t (_, e) -> Indexing.index t e)
         Indexing.empty active
     in
-    let res = forward_simplify env (Positive, e) (active, tbl) in
+    let res = forward_simplify eq_uri env (Positive, e) (active, tbl) in
     match others with
         | hd::tl -> (
             match res with
@@ -1951,6 +1677,7 @@ let main_demod_equalities dbd term metasenv ugraph =
   let goal' = List.nth goals 0 in
   let _, metasenv, meta_proof, _ = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let eq_uri = eq_of_goal goal in 
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let lib_eq_uris, library_equalities, maxm =
     find_library_equalities dbd context (proof, goal') (maxm+2)
@@ -1972,7 +1699,9 @@ let main_demod_equalities dbd term metasenv ugraph =
   (*try*)
     let goal = [], [], goal 
     in
-    let equalities = simplify_equalities env (equalities@library_equalities) in
+    let equalities = 
+      simplify_equalities eq_uri env (equalities@library_equalities) 
+    in
     let active = make_active () in
     let passive = make_passive equalities in
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
@@ -1986,7 +1715,7 @@ let main_demod_equalities dbd term metasenv ugraph =
     start_time := Unix.gettimeofday ();
     if !time_limit < 1. then time_limit := 60.;    
     let ra, rp =
-      saturate_equations env goal (fun e -> true) passive active
+      saturate_equations eq_uri env goal (fun e -> true) passive active
     in
 
     let initial =
@@ -2012,7 +1741,9 @@ let main_demod_equalities dbd term metasenv ugraph =
          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
 (*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
       (String.concat "\n"
-         (List.map (fun e -> CicPp.ppterm (Equality.term_of_equality e)) passive));
+         (List.map 
+           (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) 
+          passive));
     print_newline ();
 (*
   with e ->
@@ -2024,7 +1755,10 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   let module I = Inference in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let eq_indexes, equalities, maxm = I.find_equalities context proof in
+  let eq_uri = eq_of_goal ty in 
+  let eq_indexes, equalities, maxm = 
+    Inference.find_equalities context proof 
+  in
   let lib_eq_uris, library_equalities, maxm =
     I.find_library_equalities dbd context (proof, goal) (maxm+2) in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
@@ -2032,7 +1766,9 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   let library_equalities = List.map snd library_equalities in
   let initgoal = [], [], ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
-  let equalities = simplify_equalities env (equalities@library_equalities) in   
+  let equalities = 
+    simplify_equalities eq_uri env (equalities@library_equalities) 
+  in   
   let table = 
     List.fold_left 
       (fun tbl eq -> Indexing.index tbl eq) 
@@ -2046,7 +1782,8 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
     begin
       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
       let proofterm,_ = 
-        Equality.build_goal_proof newproof opengoal ty [] in
+        Equality.build_goal_proof eq_uri newproof opengoal ty [] 
+      in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
           (curi,extended_metasenv,pbo,pty),goal in
diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index c2b1905f8..8b67ddb05 100644
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -724,19 +724,6 @@ let string_of_pos = function
   | Right -> "Right"
 ;;
 
-let eq_URI () =
- match LibraryObjects.eq_URI () with
-    None -> assert false
-  | Some uri -> uri
-
-let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(eq_URI ())
-let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(eq_URI ())
-let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(eq_URI ())
-let eq_XURI () =
-  let s = UriManager.string_of_uri (eq_URI ()) in
-  UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(eq_URI ())
-
 let metas_of_term t = 
   List.map fst (CicUtil.metas_of_term t)
 ;;
diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli
index 2f1533e69..5e3f61e1a 100644
--- a/components/tactics/paramodulation/utils.mli
+++ b/components/tactics/paramodulation/utils.mli
@@ -87,12 +87,4 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int
 
 val debug_print: string Lazy.t -> unit
 
-val eq_URI: unit -> UriManager.uri
-val eq_ind_URI: unit -> UriManager.uri
-val eq_ind_r_URI: unit -> UriManager.uri
-val sym_eq_URI: unit -> UriManager.uri
-val eq_XURI: unit -> UriManager.uri
-val trans_eq_URI: unit -> UriManager.uri
-
 val metas_of_term: Cic.term -> int list
-
-- 
2.39.2