From 102b6ad309695168ae95c2d4a9c3daa96599de21 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 27 Mar 2006 15:02:32 +0000
Subject: [PATCH] args removed from equalities. New selection strategy. De
 morgan: 253 s.

---
 .../paramodulation/equality_indexing.ml       | 12 +--
 components/tactics/paramodulation/indexing.ml | 50 +++++-----
 .../tactics/paramodulation/indexing.mli       |  2 +-
 .../tactics/paramodulation/inference.ml       | 38 ++++----
 .../tactics/paramodulation/inference.mli      |  3 +-
 .../tactics/paramodulation/saturation.ml      | 93 +++++++++++++------
 components/tactics/tactics.mli                |  2 +-
 7 files changed, 111 insertions(+), 89 deletions(-)

diff --git a/components/tactics/paramodulation/equality_indexing.ml b/components/tactics/paramodulation/equality_indexing.ml
index 1dffb6399..4c07731d5 100644
--- a/components/tactics/paramodulation/equality_indexing.ml
+++ b/components/tactics/paramodulation/equality_indexing.ml
@@ -58,7 +58,7 @@ struct
     ;;
 
     let remove_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	match ordering with
 	  | Utils.Gt -> remove_index tree l (Utils.Left, equality)
 	  | Utils.Lt -> remove_index tree r (Utils.Right, equality)
@@ -67,7 +67,7 @@ struct
 		remove_index tree l (Utils.Left, equality)
 
     let index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	match ordering with
 	  | Utils.Gt -> index tree l (Utils.Left, equality)
 	  | Utils.Lt -> index tree r (Utils.Right, equality)
@@ -77,7 +77,7 @@ struct
   
 
     let in_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
       let meta_convertibility (pos,equality') = 
 	Inference.meta_convertibility_eq equality equality' 
       in
@@ -103,7 +103,7 @@ module PT =
     ;;
 
     let remove_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	  match ordering with
 	  | Utils.Gt -> remove_index tree l (Utils.Left, equality)
 	  | Utils.Lt -> remove_index tree r (Utils.Right, equality)
@@ -112,7 +112,7 @@ module PT =
 		remove_index tree l (Utils.Left, equality)
 
     let index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
 	match ordering with
 	  | Utils.Gt -> index tree l (Utils.Left, equality)
 	  | Utils.Lt -> index tree r (Utils.Right, equality)
@@ -122,7 +122,7 @@ module PT =
   
 
     let in_index tree equality = 
-      let _, _, (_, l, r, ordering), _, _ = equality in
+      let _, _, (_, l, r, ordering), _ = equality in
       let meta_convertibility (pos,equality') = 
 	Inference.meta_convertibility_eq equality equality' 
       in
diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index bbc605620..48abdf84e 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -112,13 +112,7 @@ let check_disjoint_invariant subst metasenv msg =
 ;;
 
 let check_for_duplicates metas msg =
-let _ = 
-    try
-      ignore(CicUtil.lookup_meta 190 metas);
-      prerr_endline ("eccoci in " ^ msg);
-    with
-	CicUtil.Meta_not_found _ -> () in
-if List.length metas <> 
+  if List.length metas <> 
   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
     begin 
       prerr_endline ("DUPLICATI " ^ msg);
@@ -137,7 +131,7 @@ let check_res res msg =
 ;;
 
 let check_target context target msg =
-  let w, proof, (eq_ty, left, right, order), metas, args = target in
+  let w, proof, (eq_ty, left, right, order), metas = target in
   (* check that metas does not contains duplicates *)
   let eqs = Inference.string_of_equality target in
   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
@@ -246,7 +240,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
   function
     | [] -> None
     | candidate::tl ->
-        let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, proof, (ty, left, right, o), metas) = candidate in
         if Utils.debug_metas then 
 	  ignore(check_target context (snd candidate) "find_matches");
         if Utils.debug_res then 
@@ -334,7 +328,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   function
     | [] -> []
     | candidate::tl ->
-        let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, _, (ty, left, right, o), metas) = candidate in
         let do_match c eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -398,7 +392,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   returns true if target is subsumed by some equality in table
 *)
 let subsumption env table target =
-  let _, _, (ty, left, right, _), tmetas, _ = target in
+  let _, _, (ty, left, right, _), tmetas = target in
   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =
@@ -424,7 +418,7 @@ let subsumption env table target =
   in
   let rec ok what = function
     | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
+    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
@@ -585,14 +579,14 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, proof, (eq_ty, left, right, order), metas, args = target in
+  let w, proof, (eq_ty, left, right, order), metas = target in
   (* first, we simplify *)
   let right = U.guarded_simpl context right in
   let left = U.guarded_simpl context left in
   let order = !Utils.compare_terms left right in
   let stat = (eq_ty, left, right, order) in 
   let w = Utils.compute_equality_weight stat in
-  let target = w, proof, stat, metas, args in
+  let target = w, proof, stat, metas in
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -608,7 +602,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
         let substs = CicMetaSubst.ppsubst subst in 
 	ignore(check_target context (snd eq_found) ("input3" ^ substs))
       end;
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let ty =
     try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
@@ -647,8 +641,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
             let what, other =
               if pos = Utils.Left then what, other else other, what
             in
-            pos, (0, proof', (ty, other, what, Utils.Incomparable),
-                  menv', args')
+            pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
           in
           let target_proof =
             let pb =
@@ -697,7 +690,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
       let w = Utils.compute_equality_weight stat in
-      (w, newproof, stat,newmenv,args) in
+      (w, newproof, stat,newmenv) in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
@@ -873,7 +866,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
+  let weight, proof, (eq_ty, left, right, ordering), menv = target in
   if Utils.debug_metas then
     ignore(check_target context target "superpositionleft");
   let expansions, _ =
@@ -891,7 +884,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
@@ -920,7 +913,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
       in
       let target_proof =
         let pb =
@@ -953,7 +946,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
     let w = Utils.compute_equality_weight stat in
-    (w, newproof, stat, newmenv, []) 
+    (w, newproof, stat, newmenv) 
 
   in
   !maxmeta, List.map build_new expansions
@@ -976,7 +969,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in 
-  let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in 
+  let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in 
   if Utils.debug_metas then 
     ignore (check_target context target "superpositionright");
   let metasenv' = newmetas in
@@ -1008,7 +1001,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       ignore (check_target context (snd eq_found) "buildnew1" );
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       (* qua *)
@@ -1030,11 +1023,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         else apply_subst s left, newgoal in
       let neworder = !Utils.compare_terms left right in
       let newmenv = (* Inference.filter s *) m in
-      let newargs = args @ args' in
       let stat = (eq_ty, left, right, neworder) in
       let eq' =
         let w = Utils.compute_equality_weight stat in
-        (w, newproof, stat, newmenv, newargs) in
+        (w, newproof, stat, newmenv) in
       if Utils.debug_metas then 
 	ignore (check_target context eq' "buildnew3");
       let newm, eq' = Inference.fix_metas !maxmeta eq' in
@@ -1071,7 +1063,7 @@ let rec demodulation_goal newmeta env table goal =
   let metasenv' = metas in
 
   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let ty =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
@@ -1100,7 +1092,7 @@ let rec demodulation_goal newmeta env table goal =
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
       in
       let goal_proof =
         let pb =
@@ -1155,7 +1147,7 @@ let rec demodulation_theorem newmeta env table theorem =
   let metasenv' = metas in
   
   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newty =
       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index bb005f8d3..4d99385ed 100644
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -48,7 +48,7 @@ val build_newtarget_time : float ref
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  'a * 'b * ('c * Index.key * Index.key * 'd) * Cic.metasenv * 'e ->
+  Inference.equality ->
   bool * Cic.substitution
 val superposition_left :
   int ->
diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index f5508c8c1..6582bfd25 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -37,8 +37,7 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof (* term is the goal missing a proof *)
@@ -55,14 +54,14 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | w, _, (ty, left, right, o), _ ->
             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
     )
   | Some (_, context, _) -> (
       let names = names_of_context context in
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | w, _, (ty, left, right, o), _ ->
             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
               (CicPp.pp left names) (string_of_comparison o)
               (CicPp.pp right names)
@@ -139,11 +138,11 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
         let t' = Cic.Lambda (name, ty, bo) in
         let proof' =
-          let _, proof', _, _, _ = eq in
+          let _, proof', _, _ = eq in
           do_build_proof proof'
         in
         let eqproof = do_build_proof eqproof in
-        let _, _, (ty, what, other, _), menv', args' = eq in
+        let _, _, (ty, what, other, _), menv' = eq in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
@@ -311,8 +310,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, _, (ty, left, right, _), _, _ = eq1
-  and _, _, (ty', left', right', _), _, _ = eq2 in
+  let _, _, (ty, left, right, _), _ = eq1
+  and _, _, (ty', left', right', _), _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -726,7 +725,7 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 let matching = matching1;;
 
 let check_eq context msg eq =
-  let w, proof, (eq_ty, left, right, order), metas, args = eq in
+  let w, proof, (eq_ty, left, right, order), metas = eq in
   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
    CicUniv.empty_ugraph))
@@ -773,7 +772,7 @@ let find_equalities context proof =
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -785,7 +784,7 @@ let find_equalities context proof =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof (C.Rel index), stat, [], []) in
+              let e = (w, BasicProof (C.Rel index), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -923,7 +922,7 @@ let find_library_equalities dbd context status maxmeta =
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -932,7 +931,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof term, stat, [], []) in
+              let e = (w, BasicProof term, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1135,7 +1134,7 @@ let relocate newmeta menv =
   subst, metasenv, newmeta
 
 
-let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
   (*
   let metas = (metas_of_term left)@(metas_of_term right)
     @(metas_of_term ty)@(metas_of_proof p) in
@@ -1149,7 +1148,6 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
   let ty = CicMetaSubst.apply_subst subst ty in
   let left = CicMetaSubst.apply_subst subst left in
   let right = CicMetaSubst.apply_subst subst right in
-  let args = List.map (CicMetaSubst.apply_subst subst) args in
   let rec fix_proof = function
     | NoProof -> NoProof 
     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
@@ -1171,7 +1169,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
     @(metas_of_term ty)@(metas_of_proof p) in
   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
   *)
-  let eq = (w, p, (ty, left, right, o), metasenv, args) in
+  let eq = (w, p, (ty, left, right, o), metasenv) in
   (* debug prerr_endline (string_of_equality eq); *)
   newmeta+1, eq  
 
@@ -1193,7 +1191,7 @@ let equality_of_term proof term =
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = compute_equality_weight stat in
-      let e = (w, BasicProof proof, stat, [], []) in
+      let e = (w, BasicProof proof, stat, []) in
       e
   | _ ->
       raise TermIsNotAnEquality
@@ -1203,7 +1201,7 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 let is_weak_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) -> 
+  | (_, _, (ty, left, right, _), menv) -> 
        (left = right ||
           (meta_convertibility left right)) 
 	   (* the test below is not a good idea since it stops
@@ -1213,7 +1211,7 @@ let is_weak_identity (metasenv, context, ugraph) = function
 ;;
 
 let is_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) ->
+  | (_, _, (ty, left, right, _), menv) ->
        (left = right ||
           (* (meta_convertibility left right)) *)
            (fst (CicReduction.are_convertible 
@@ -1222,7 +1220,7 @@ let is_identity (metasenv, context, ugraph) = function
 
 
 let term_of_equality equality =
-  let _, _, (ty, left, right, _), menv, _ = equality in
+  let _, _, (ty, left, right, _), menv = equality in
   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
   let argsno = List.length menv in
   let t =
diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli
index 5fdf694fc..dd2d4caa1 100644
--- a/components/tactics/paramodulation/inference.mli
+++ b/components/tactics/paramodulation/inference.mli
@@ -32,8 +32,7 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof   (* no proof *)
diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b6678683d..bf9f8ba57 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -32,7 +32,7 @@ open Utils;;
 (*
 for debugging 
 let check_equation env equation msg =
-  let w, proof, (eq_ty, left, right, order), metas, args = equation in
+  let w, proof, (eq_ty, left, right, order), metas = equation in
   let metasenv, context, ugraph = env in
   let metasenv' = metasenv @ metas in
     try
@@ -101,7 +101,7 @@ type goal = proof * Cic.metasenv * Cic.term;;
 
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
-let symbols_of_equality (_, _, (_, left, right, _), _, _) =
+let symbols_of_equality (_, _, (_, left, right, _), _) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -116,26 +116,57 @@ let symbols_of_equality (_, _, (_, left, right, _), _, _) =
   m
 ;;
 
-module OrderedEquality = struct
+(* griggio *)
+module OrderedEquality = struct 
   type t = Inference.equality
 
   let compare eq1 eq2 =
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let w1, _, (ty, left, right, _), _, a = eq1
-        and w2, _, (ty', left', right', _), _, a' = eq2 in
+        let w1, _, (ty, left, right, _), m1 = eq1
+        and w2, _, (ty', left', right', _), m2 = eq2 in
         match Pervasives.compare w1 w2 with
+        | 0 -> 
+	    let res = (List.length m1) - (List.length m2) in 
+            if res <> 0 then res else Pervasives.compare eq1 eq2
+        | res -> res 
+end 
+
+(*
+module OrderedEquality = struct
+  type t = Inference.equality
+
+  let minor eq =
+    let w, _, (ty, left, right, o), _ = eq in
+      match o with
+	 | Lt -> Some left
+	 | Le -> assert false
+	 | Gt -> Some right
+	 | Ge -> assert false
+	 | Eq 
+	 | Incomparable -> None
+	     
+  let compare eq1 eq2 =
+    let w1, _, (ty, left, right, o1), m1 = eq1
+    and w2, _, (ty', left', right', o2), m2 = eq2 in
+      match Pervasives.compare w1 w2 with
         | 0 ->
-            let res = (List.length a) - (List.length a') in
-            if res <> 0 then res else (
-              try
-                let res = Pervasives.compare (List.hd a) (List.hd a') in
-                if res <> 0 then res else Pervasives.compare eq1 eq2
-              with Failure "hd" -> Pervasives.compare eq1 eq2
-            )
-        | res -> res
+	    (match minor eq1, minor eq2 with
+	      | Some t1, Some t2 ->
+		  fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
+	      | Some _, None -> -1
+	      | None, Some _ -> 1
+	      | _,_ -> 
+	          (List.length m2) - (List.length m1) )
+	| res ->  res
+  
+  let compare eq1 eq2 =
+    match compare eq1 eq2 with
+	0 -> Pervasives.compare eq1 eq2
+      | res -> res 
 end 
+*)
 
 module EqualitySet = Set.Make(OrderedEquality);;
 
@@ -208,7 +239,7 @@ let rec select env goals passive (active, _) =
           (Negative, hd),
           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
       | [], (hd:EqualitySet.elt)::tl ->
-          let w,_,_,_,_ = hd in
+          let w,_,_,_ = hd in
           let passive_table =
 	    Indexing.remove_index passive_table hd
           in  (Positive, hd),
@@ -261,7 +292,7 @@ let rec select env goals passive (active, _) =
   | _ ->
       symbols_counter := !symbols_ratio;
       let set_selection set = EqualitySet.min_elt set in 
-      (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *)
+      (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l in *)
       if EqualitySet.is_empty neg_set then
         let current = set_selection pos_set in
         let passive =
@@ -546,7 +577,7 @@ let contains_empty env (negative, positive) =
   try
     let found =
       List.find
-        (fun (w, proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -733,7 +764,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
   let active_list, newa = 
     List.fold_right
       (fun (s, equality) (res, newn) ->
-         let ew, _, _, _, _ = equality in
+         let ew, _, _, _ = equality in
          if ew < min_weight then
            (s, equality)::res, newn
          else
@@ -779,7 +810,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
 let backward_simplify_passive env new_pos new_table min_weight passive =
   let (nl, ns), (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
-    let ew, _, _, _, _ = equality in
+    let ew, _, _, _ = equality in
     if ew < min_weight then
       equality::resl, ress, newn
     else
@@ -808,7 +839,7 @@ let backward_simplify env new' ?passive active =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
-         let ew, _, _, _, _ = e in
+         let ew, _, _, _ = e in
          (Positive, e)::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) (snd new')
   in
@@ -830,7 +861,7 @@ let close env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
-         let ew, _, _, _, _ = e in
+         let ew, _, _, _ = e in
          (Positive, e)::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) (snd new')
   in
@@ -842,7 +873,7 @@ let close env new' given =
 ;;
 
 let is_commutative_law eq =
-  let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+  let w, proof, (eq_ty, left, right, order), metas = snd eq in
     match left,right with
 	Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], 
 	Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
@@ -1041,7 +1072,7 @@ let apply_equality_to_goal env equality goal =
   let module HL = HelmLibraryObjects in
   let module I = Inference in
   let metasenv, context, ugraph = env in
-  let _, proof, (ty, left, right, _), metas, args = equality in
+  let _, proof, (ty, left, right, _), metas = equality in
   let eqterm =
     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
@@ -1630,7 +1661,7 @@ and given_clause_aux dbd env goals theorems passive active =
             debug_print
               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                        (string_of_equality ~env current)));
-            let _, proof, _, _, _  = current in
+            let _, proof, _, _ = current in
             ParamodulationSuccess (Some proof, env)
           ) else (           
             debug_print
@@ -1648,7 +1679,7 @@ and given_clause_aux dbd env goals theorems passive active =
             if res then
               let proof =
                 match goal' with
-                | Some goal -> let _, proof, _, _, _ = goal in Some proof
+                | Some goal -> let _, proof, _, _ = goal in Some proof
                 | None -> None
               in
               ParamodulationSuccess (proof, env)
@@ -1700,7 +1731,7 @@ and given_clause_aux dbd env goals theorems passive active =
                   let proof =
                     match goal with
                     | Some goal ->
-                        let _, proof, _, _, _ = goal in Some proof
+                        let _, proof, _, _ = goal in Some proof
                     | None -> None
                   in
                   ParamodulationSuccess (proof, env)
@@ -1740,6 +1771,7 @@ let rec given_clause_fullred dbd env goals theorems passive active =
         | _ -> assert false
       in
       ( prerr_endline "esco qui";
+        (*
 	let s = Printf.sprintf "actives:\n%s\n"
 	  (String.concat "\n"
              ((List.map
@@ -1752,7 +1784,7 @@ let rec given_clause_fullred dbd env goals theorems passive active =
 		(string_of_equality ~env)
 		(let x,y,_ = passive in (fst x)@(fst y)))) in
 	  prerr_endline s;
-	  prerr_endline sp;
+	  prerr_endline sp; *)
       ParamodulationSuccess (proof, env))
     else
       given_clause_fullred_aux dbd env goals theorems passive active
@@ -1778,6 +1810,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                  " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
 		 " #ACTIVES: " ^ string_of_int (size_of_active active) ^
                  " #PASSIVES: " ^ string_of_int (size_of_passive passive));
+(*
   if (size_of_active active) mod 50 = 0 then
     (let s = Printf.sprintf "actives:\n%s\n"
       (String.concat "\n"
@@ -1791,7 +1824,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
              (string_of_equality ~env)
              (let x,y,_ = passive in (fst x)@(fst y)))) in
       prerr_endline s;
-      prerr_endline sp);
+      prerr_endline sp); *)
   let time1 = Unix.gettimeofday () in
   let (_,context,_) = env in
   let selection_estimate = get_selection_estimate () in
@@ -1839,7 +1872,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
             debug_print
               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                        (string_of_equality ~env current)));
-            let _, proof, _, _, _ = current in 
+            let _, proof, _, _ = current in 
             ParamodulationSuccess (Some proof, env)
           ) else (
             debug_print
@@ -1954,7 +1987,7 @@ end prova *)
             | true, goal ->
                 let proof =
                   match goal with
-                  | Some goal -> let _, proof, _, _, _ = goal in Some proof
+                  | Some goal -> let _, proof, _, _ = goal in Some proof
                   | None -> None
                 in
                 ParamodulationSuccess (proof, env)
@@ -2132,7 +2165,7 @@ let main dbd full term metasenv ugraph =
             print_endline (PP.pp proof names);
             let newmetasenv =
               List.fold_left
-                (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+                (fun m (_, _, _, menv) -> m @ menv) metasenv equalities
             in
             let _ =
               (*try*)
diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 751d9e93f..60a485bce 100644
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Mar 21 17:18:22 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 27 15:17:54 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
-- 
2.39.2