From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 4 Apr 2006 15:01:30 +0000 (+0000)
Subject: Naif substitution. Removed local context in metas during relocation.
X-Git-Tag: 0.4.95@7852~1535
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbdd5bb6ea9a29c0a06bf29c6ff5db684c8ca0e9;p=helm.git

Naif substitution. Removed local context in metas during relocation.
Removed apply_theorems in saturate, replaced by a local check for
identity.
---

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index b4cf802d0..f61202396 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -93,7 +93,7 @@ let print_candidates ?env mode term res =
 let indexing_retrieval_time = ref 0.;;
 
 
-let apply_subst = CicMetaSubst.apply_subst
+let apply_subst = Inference.apply_subst
 
 let index = Index.index
 let remove_index = Index.remove_index
@@ -136,7 +136,7 @@ let check_target context target msg =
   let eqs = Inference.string_of_equality target in
   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
   let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
-    @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
+    @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof)  in
   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
   let _ = if menv <> metas then 
     begin 
@@ -148,19 +148,20 @@ let check_target context target msg =
       prerr_endline ("right: " ^ (CicPp.ppterm right)); 
       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
       assert false
-    end 
-  else () in
+    end
+  else () in ()
+(*
   try 
-      CicTypeChecker.type_of_aux'
-        metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
+      ignore(CicTypeChecker.type_of_aux'
+	metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
   with e ->  
       prerr_endline msg;
       prerr_endline (Inference.string_of_proof proof);
       prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); 
-      raise e
-;;
+      raise e 
+*)
 
 
 (* returns a list of all the equalities in the tree that are in relation
@@ -409,16 +410,15 @@ let find_all_matches
 let subsumption env table target =
   let _, _, (ty, left, right, _), tmetas = target in
   let metasenv, context, ugraph = env in
-  let metasenv = metasenv @ tmetas in
+  let metasenv = tmetas in
   let samesubst subst subst' =
     let tbl = Hashtbl.create (List.length subst) in
-    List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
+    List.iter (fun (m, x) -> Hashtbl.add tbl m x) subst;
     List.for_all
-      (fun (m, (c, t1, t2)) ->
+      (fun (m, x) ->
          try
-           let c', t1', t2' = Hashtbl.find tbl m in
-           if (c = c') && (t1 = t1') && (t2 = t2') then true
-           else false
+           let x' = Hashtbl.find tbl m in
+           x = x'
          with Not_found ->
            true)
       subst'
@@ -488,7 +488,14 @@ let rec demodulation_aux ?from ?(typecheck=false)
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let candidates = 
-    get_candidates ~env:(metasenv,context,ugraph) Matching table term in
+    get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
+  if List.exists (fun (i,_,_) -> i = 2840) metasenv
+  then
+    (prerr_endline ("term: " ^(CicPp.ppterm term));
+     List.iter (fun (_,x) -> prerr_endline (Inference.string_of_equality  x))
+       candidates;
+     prerr_endline ("-------");
+     prerr_endline ("+++++++"));
 (*   let candidates = List.map make_variant candidates in *)
   let res =
     match term with
@@ -616,7 +623,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
       begin
         ignore(check_for_duplicates menv "input1");
         ignore(check_disjoint_invariant subst menv "input2");
-        let substs = CicMetaSubst.ppsubst subst in 
+        let substs = Inference.ppsubst subst in 
         ignore(check_target context (snd eq_found) ("input3" ^ substs))
       end;
     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
@@ -639,6 +646,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
            Inference.ProofBlock (
              subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
       else
+	begin
+        prerr_endline "***************************************negative";
         let metaproof = 
           incr maxmeta;
           let irl =
@@ -662,15 +671,15 @@ let rec demodulation_equality ?from newmeta env table sign target =
           in
           let target_proof =
             let pb =
-              Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
-                                    eq_found, Inference.BasicProof metaproof)
+              Inference.ProofBlock 
+		(subst, eq_URI, (name, ty), bo',
+                 eq_found, Inference.BasicProof ([],metaproof))
             in
             match proof with
             | Inference.BasicProof _ ->
                 (* print_endline "replacing a BasicProof"; *)
                 pb
             | Inference.ProofGoalBlock (_, parent_proof) ->
-              
   (* print_endline "replacing another ProofGoalBlock"; *)
                 Inference.ProofGoalBlock (pb, parent_proof)
             | _ -> assert false
@@ -681,7 +690,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   eq_ty; if is_left then right else left]          
         in
         (bo,
-         Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
+         Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
+	end
     in
     let newmenv = (* Inference.filter subst *) menv in
     let _ = 
@@ -691,12 +701,12 @@ let rec demodulation_equality ?from newmeta env table sign target =
           () 
         with exc ->                   
           prerr_endline "sempre lui";
-          prerr_endline (CicMetaSubst.ppsubst subst);
+          prerr_endline (Inference.ppsubst subst);
           prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
-          prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
+          prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
           raise exc;
       else () 
     in
@@ -943,7 +953,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
       let target_proof =
         let pb =
           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
-                                Inference.BasicProof metaproof)
+                                Inference.BasicProof ([],metaproof))
         in
         match proof with
         | Inference.BasicProof _ ->
@@ -960,7 +970,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
                 eq_ty; if ordering = U.Gt then right else left]
       in
       (bo',
-       Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
+       Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
     in
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
@@ -1086,7 +1096,7 @@ let rec demodulation_goal newmeta env table goal =
   let term = Utils.guarded_simpl (~debug:true) context term in
   let goal = proof, metas, term in
   let metasenv' = metas in
-
+  
   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
@@ -1122,7 +1132,7 @@ let rec demodulation_goal newmeta env table goal =
       let goal_proof =
         let pb =
           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
-                                eq_found, Inference.BasicProof metaproof)
+                                eq_found, Inference.BasicProof ([],metaproof))
         in
         let rec repl = function
           | Inference.NoProof ->
@@ -1135,6 +1145,7 @@ let rec demodulation_goal newmeta env table goal =
 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
               Inference.ProofGoalBlock (pb, parent_proof)
           | Inference.SubProof (term, meta_index, p)  ->
+              prerr_endline "subproof!";
               Inference.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof
@@ -1180,12 +1191,10 @@ let rec demodulation_theorem newmeta env table theorem =
       incr demod_counter;
       let newproof =
         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
-                              Inference.BasicProof term)
+                              Inference.BasicProof ([],term))
       in
       (Inference.build_proof_term newproof, bo)
     in    
-    
-    (* let m = Inference.metas_of_term newterm in *)
     !maxmeta, (newterm, newty, menv)
   in  
   let res =
diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index 4d99385ed..d10d7e6d8 100644
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -49,7 +49,7 @@ val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Inference.equality ->
-  bool * Cic.substitution
+  bool * Inference.substitution
 val superposition_left :
   int ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
@@ -84,7 +84,7 @@ val demodulation_theorem :
   'a * (Cic.term * Index.key * Cic.metasenv)
 val check_target:
   Cic.context ->
-    Inference.equality -> string -> Cic.term * CicUniv.universe_graph
+    Inference.equality -> string -> unit
 
 (* maxmeta for relocate *)
 val local_max : int ref
diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index e2f21b25c..f74cd1797 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -26,9 +26,135 @@
 (* $Id$ *)
 
 open Utils;;
+open Printf;;
 
 let metas_of_proof_time = ref 0.;;
 let metas_of_term_time = ref 0.;;
+(*
+type substitution = Cic.substitution 
+let apply_subst = CicMetaSubst.apply_subst
+let apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
+let ppsubst = CicMetaSubst.ppsubst
+let buildsubst n context t ty = (n,(context,t,ty))
+let flatten_subst subst =
+    List.map
+      (fun (i, (context, term, ty)) ->
+	 let context = (*` apply_subst_context subst*) context in
+	 let term = apply_subst subst term in
+	 let ty = apply_subst subst ty in  
+	 (i, (context, term, ty))) subst
+let rec lookup_subst meta subst =
+  match meta with
+  | Cic.Meta (i, _) -> (
+      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
+      in lookup_subst t subst 
+      with Not_found -> meta
+    )
+  | _ -> meta
+;;
+*)
+
+(* naif version of apply subst; the local context of metas is ignored;
+we assume the substituted term must be lifted according to the nesting
+depth of the meta. Alternatively, ee could used implicit instead of
+metas *)
+
+
+type substitution = (int * Cic.term) list 
+
+let apply_subst subst term =
+ let rec aux k t =
+   match t with
+       Cic.Rel _ -> t
+     | Cic.Var (uri,exp_named_subst) -> 
+	 let exp_named_subst' =
+           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	 in
+	   Cic.Var (uri, exp_named_subst')
+    | Cic.Meta (i, l) -> 
+        (try
+          aux k (CicSubstitution.lift k (List.assoc i subst)) 
+         with Not_found -> t)
+    | Cic.Sort _
+    | Cic.Implicit _ -> t
+    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
+    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
+    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
+    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+    | Cic.Appl [] -> assert false
+    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
+    | Cic.Const (uri,exp_named_subst) ->
+	let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	in
+	  if exp_named_subst' != exp_named_subst then
+	    Cic.Const (uri, exp_named_subst')
+	  else
+	    t (* TODO: provare a mantenere il piu' possibile sharing *)
+    | Cic.MutInd (uri,typeno,exp_named_subst) ->
+	let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	in
+	  Cic.MutInd (uri,typeno,exp_named_subst')
+    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+	let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	in
+	  Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | Cic.MutCase (sp,i,outty,t,pl) ->
+	let pl' = List.map (aux k) pl in
+	  Cic.MutCase (sp, i, aux k outty, aux k t, pl')
+    | Cic.Fix (i, fl) ->
+	let len = List.length fl in
+	let fl' =
+         List.map 
+	   (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
+	in
+	  Cic.Fix (i, fl')
+    | Cic.CoFix (i, fl) ->
+	let len = List.length fl in
+	let fl' =
+          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
+	in
+	  Cic.CoFix (i, fl')
+in
+  aux 0 term
+;;
+
+(* naif version of apply_subst_metasenv: we do not apply the 
+substitution to the context *)
+
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.mem_assoc i subst))
+      metasenv)
+
+let ppsubst subst =
+  String.concat "\n"
+    (List.map
+      (fun (idx, t) ->
+         sprintf "%d:= %s" idx (CicPp.ppterm t))
+       subst)
+;;
+
+let buildsubst n context t ty = (n,t) ;;
+
+let flatten_subst subst = 
+  List.map (fun (i,t) -> i, apply_subst subst t ) subst
+;;
+
+let rec lookup_subst meta subst =
+  match meta with
+    | Cic.Meta (i, _) ->
+	(try
+	  lookup_subst (List.assoc i subst) subst
+	with
+	    Not_found -> meta)
+    | _ -> meta
+;;
 
 type equality =
     int  *               (* weight *)
@@ -41,9 +167,9 @@ type equality =
 
 and proof =
   | NoProof (* term is the goal missing a proof *)
-  | BasicProof of Cic.term
+  | BasicProof of substitution * Cic.term
   | ProofBlock of
-      Cic.substitution * UriManager.uri *
+      substitution * UriManager.uri *
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof 
   | ProofSymBlock of Cic.term list * proof
@@ -71,13 +197,14 @@ let string_of_equality ?env =
 
 let rec string_of_proof = function
   | NoProof -> "NoProof " 
-  | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+  | BasicProof (s, t) -> "BasicProof " ^ 
+      (CicPp.ppterm (apply_subst s t))
   | SubProof (t, i, p) ->
       Printf.sprintf "SubProof(%s, %s, %s)"
         (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
   | ProofSymBlock _ -> "ProofSymBlock"
   | ProofBlock (subst, _, _, _ ,_,_) -> 
-      "ProofBlock" ^ (CicMetaSubst.ppsubst subst)
+      "ProofBlock" ^ (ppsubst subst)
   | ProofGoalBlock (p1, p2) ->
       Printf.sprintf "ProofGoalBlock(%s, %s)"
         (string_of_proof p1) (string_of_proof p2)
@@ -127,7 +254,7 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
     | NoProof ->
         Printf.fprintf stderr "WARNING: no proof!\n";
         noproof
-    | BasicProof term -> term
+    | BasicProof (s,term) -> apply_subst s term
     | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
         do_build_goal_proof proofbit proof
@@ -146,7 +273,7 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        CicMetaSubst.apply_subst subst
+        apply_subst subst
           (Cic.Appl [Cic.Const (eq_URI, []); ty;
                      what; t'; eqproof; other; proof'])
     | SubProof (term, meta_index, proof) ->
@@ -176,10 +303,9 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
         SubProof (term, meta_index, replace_proof newproof p)
     | p -> p
   in
-  do_build_proof proof
+  do_build_proof proof 
 ;;
 
-
 let rec metas_of_term = function
   | Cic.Meta (i, c) -> [i]
   | Cic.Var (_, ens) 
@@ -217,6 +343,7 @@ let rec metas_of_proof p =
     metas_of_term (build_proof_term p)
 ;;
 
+
 exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
@@ -365,17 +492,6 @@ let rec is_simple_term = function
   | _ -> false
 ;;
 
-
-let rec lookup_subst meta subst =
-  match meta with
-  | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
-      in lookup_subst t subst 
-      with Not_found -> meta
-    )
-  | _ -> meta
-;;
-
 let locked menv i =
   List.exists (fun (j,_,_) -> i = j) menv
 ;;
@@ -419,7 +535,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
           assert (not (List.mem_assoc i subst));
-	  let subst = (i, (context, t, ty))::subst in
+	  let subst = (buildsubst i context t ty)::subst in
           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
@@ -474,33 +590,16 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   in
   if Utils.debug_res then
 	    ignore(check_disjoint_invariant subst menv "unif");
-  let flatten subst = 
+  (* let flatten subst = 
     List.map
       (fun (i, (context, term, ty)) ->
-	 let context = CicMetaSubst.apply_subst_context subst context in
-	 let term = CicMetaSubst.apply_subst subst term in
-	 let ty = CicMetaSubst.apply_subst subst ty in  
+	 let context = apply_subst_context subst context in
+	 let term = apply_subst subst term in
+	 let ty = apply_subst subst ty in  
 	   (i, (context, term, ty))) subst 
   in
-  let flatten_fast subst = 
-    let resolve_meta (i, (context, term, ty)) subst = 
-	    let term = CicMetaSubst.apply_subst subst term in
-	    let ty = CicMetaSubst.apply_subst subst ty in  
-	     (i, (context, term, ty))
-    in
-    let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in
-    let filter j (i,_) = i <> j in
-    let filter a b = profiler4.HExtlib.profile (filter a) b in
-    List.fold_left 
-      (fun subst (j,(c,t,ty)) as s ->  
-        let s = resolve_meta s subst in 
-        s::(List.filter (filter j) subst)) 
-      subst subst
-  in
-  (*let flatten subst = profiler.HExtlib.profile flatten subst in*)
-  let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in
-  (*let subst = flatten subst in*)
-(*  let subst = flatten_fast subst in*)
+  let flatten subst = profiler.HExtlib.profile flatten subst in
+  let subst = flatten subst in *)
     subst, menv, ug
 ;;
 
@@ -517,231 +616,10 @@ let matching1 metasenv1 metasenv2 context t1 t2 ugraph =
 let unification = unification_aux true 
 ;;
 
-
-
-(*
-let unification metasenv1 metasenv2 context t1 t2 ugraph = 
-  let (subst, metasenv, ugraph) = 
-    CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
-  if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "fo_unif");
-  (subst, metasenv, ugraph)
-    
-;;
-*)
-
-
-(*
-let matching_simple metasenv context t1 t2 ugraph =
-  let module C = Cic in
-  let module M = CicMetaSubst in
-  let module U = CicUnification in
-  let lookup meta subst =
-    match meta with
-    | C.Meta (i, _) -> (
-        try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
-        with Not_found -> meta
-      )
-    | _ -> assert false
-  in
-  let rec do_match subst menv s t =
-    match s, t with
-    | s, t when s = t -> subst, menv
-    | s, C.Meta (i, l) ->
-        let filter_menv i menv =
-          List.filter (fun (m, _, _) -> i <> m) menv
-        in
-        let subst, menv =
-          let value = lookup t subst in
-          match value with
-          | value when value = t ->
-              let _, _, ty = CicUtil.lookup_meta i menv in
-              (i, (context, s, ty))::subst, filter_menv i menv
-          | value when value <> s ->
-              raise MatchingFailure
-          | value -> do_match subst menv s value
-        in
-        subst, menv
-    | C.Appl ls, C.Appl lt -> (
-        try
-          List.fold_left2
-            (fun (subst, menv) s t -> do_match subst menv s t)
-            (subst, menv) ls lt
-        with Invalid_argument _ ->
-          raise MatchingFailure
-      )
-    | _, _ ->
-        raise MatchingFailure
-  in
-  let subst, menv = do_match [] metasenv t1 t2 in
-  subst, menv, ugraph
-;;
-*)
-
-(*
-let matching metasenv context t1 t2 ugraph =
-    try
-      let subst, metasenv, ugraph =
-	try
-          unification metasenv context t1 t2 ugraph
-	with CicUtil.Meta_not_found _ as exn ->
-	  Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
-	    (CicPp.ppterm t1) (CicPp.ppterm t2) 
-	    (CicMetaSubst.ppmetasenv [] metasenv);
-	  raise exn
-      in
-      if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-2");
-      let t' = CicMetaSubst.apply_subst subst t1 in
-      if not (meta_convertibility t1 t') then
-        raise MatchingFailure
-      else
-        if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-1");
-        let metas = metas_of_term t1 in
-        let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-          if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua0");
-	  
-	  let subst, metasenv =
-	  List.fold_left
-	    (fun 
-	       (subst,metasenv) s ->
-		 match s with
-		   | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-		       let metasenv' =
-			 List.filter (fun (x, _, _) -> x<>j) metasenv 
-		       in
-			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
-			  (i,c,ty)::metasenv')
-		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in
-	if Utils.debug_res then
-	  ignore(check_disjoint_invariant subst metasenv "qua1");
-(*
-        let fix_subst = function
-          | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-              (j, (c, Cic.Meta (i, lc), ty))
-          | s -> s
-        in
-        let subst = List.map fix_subst subst in *)
-	if CicMetaSubst.apply_subst subst t1 = t1 then
-          subst, metasenv, ugraph
-	else
-	  (prerr_endline "mah"; raise MatchingFailure)
-    with
-    | CicUnification.UnificationFailure _
-    | CicUnification.Uncertain _ ->
-      raise MatchingFailure
-;;
-*)
-
 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 it perform unification in the union metasenv, then check that
 the first metasenv has not changed *)
 
-
-let matching2 metasenv1 metasenv2 context t1 t2 ugraph =
-      let subst, metasenv, ugraph =
-	try
-          unification metasenv1 metasenv2 context t1 t2 ugraph
-	with 
-	    CicUtil.Meta_not_found _ as exn ->
-	      Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
-		(CicPp.ppterm t1) (CicPp.ppterm t2) 
-		(CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2));
-	      raise exn
-	  | CicUnification.UnificationFailure _
-	  | CicUnification.Uncertain _ ->
-	      raise MatchingFailure    
-      in
-      if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-2");
-      (* let us unfold subst *)
-      if metasenv = metasenv1 then 
-	let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-	  subst, metasenv, ugraph (* everything is fine *)
-      else
-	(* let us unfold subst *)
-	(* 
-	let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-        *)
-	  (* let us revert Meta-Meta in subst privileging metasenv1 *)
-	let subst, metasenv =
-	  List.fold_left
-	    (fun 
-	       (subst,metasenv) s ->
-		 match s with
-		   | (i, (c, Cic.Meta (j, lc), ty)) 
-		       when (List.exists (fun (x, _, _)  -> x=i) metasenv1) &&
-			 not (List.exists (fun (x, _)  -> x=j) subst) ->
-		       let metasenv' =
-			 List.filter (fun (x, _, _) -> x<>j) metasenv 
-		       in
-			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
-			  (i,c,ty)::metasenv')
-		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in	
-	(* finally, let us chek again that metasenv = metasenv1 *)
-	if metasenv = metasenv1 then 
-	  subst, metasenv, ugraph
-	else raise MatchingFailure  
-;;
-
-(* debug 
-let matching metasenv1 metasenv2 context t1 t2 ugraph =
-  let rc1 = 
-    try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph)
-    with MatchingFailure -> None
-  in
-  let rc2 = 
-    try 
-      Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph)
-    with MatchingFailure -> None
-  in
-  match rc1,rc2 with
-  | Some (s,m,g) , None -> 
-      prerr_endline (CicPp.ppterm t1);
-      prerr_endline (CicPp.ppterm t2);
-      prerr_endline "SOLO NOI";
-      prerr_endline (CicMetaSubst.ppsubst s);
-      s,m,g
-  | None , Some _ -> 
-      prerr_endline (CicPp.ppterm t1);
-      prerr_endline (CicPp.ppterm t2);
-      prerr_endline "SOLO LUI";
-      assert false
-  | None, None -> raise MatchingFailure 
-  | Some (s,m,g), Some (s',m',g') ->
-      let s = List.sort (fun (i,_) (j,_) -> i - j) s in
-      let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in
-      if s <> s' then 
-	begin
-	  prerr_endline (CicMetaSubst.ppsubst s);
-	  prerr_endline (CicMetaSubst.ppsubst s');
-	  prerr_endline (CicPp.ppterm t1);
-	  prerr_endline (CicPp.ppterm t2);
-	  	end;
-      s,m,g
-*)  
 let matching = matching1;;
 
 let check_eq context msg eq =
@@ -791,7 +669,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 proof = BasicProof p in
+                    let proof = BasicProof ([],p) in
                     let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -804,7 +682,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 (
@@ -912,7 +790,7 @@ let find_library_equalities dbd context status maxmeta =
     | C.LetIn (_, s, t) | C.Cast (s, t) ->
         (has_vars s) || (has_vars t)
     | _ -> false
-  in
+ in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (uri, term, termty)::tl ->
@@ -941,7 +819,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 proof = BasicProof p in
+                    let proof = BasicProof ([],p) in
                     let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -951,7 +829,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
@@ -1038,7 +916,7 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
-
+(*
 let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
   let table = Hashtbl.create (List.length args) in
 
@@ -1104,7 +982,7 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
         (Hashtbl.copy table)
   in
   let rec fix_proof = function
-    | NoProof -> NoProof 
+   | NoProof -> NoProof 
     | BasicProof term -> BasicProof (repl term)
     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
         let subst' =
@@ -1131,26 +1009,22 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
   (newmeta +1, neweq)
 ;;
-
+*)
 
 let relocate newmeta menv =
   let subst, metasenv, newmeta = 
     List.fold_right 
-      (fun (i, context, ty) (subst, menv, maxmeta) -> 
-        let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
-        let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
+      (fun (i, context, ty) (subst, menv, maxmeta) ->         
+	let irl = [] (*
+	 CicMkImplicit.identity_relocation_list_for_metavariable context *)
+	in
+        let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in
         let newmeta = maxmeta, context, ty in
         newsubst::subst, newmeta::menv, maxmeta+1) 
       menv ([], [], newmeta+1)
   in
-  let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-  let subst =
-    List.map
-      (fun (i, (context, term, ty)) ->
-	 let context = CicMetaSubst.apply_subst_context subst context in
-	 let term = CicMetaSubst.apply_subst subst term in
-	 let ty = CicMetaSubst.apply_subst subst ty in  
-	 (i, (context, term, ty))) subst in
+  let metasenv = apply_subst_metasenv subst metasenv in
+  let subst = flatten_subst subst in
   subst, metasenv, newmeta
 
 
@@ -1165,20 +1039,29 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
   prerr_endline (string_of_equality eq); *)
   let subst, metasenv, newmeta = relocate newmeta menv in
-  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 rec fix_proof = function
+(*
+  if newmeta > 2839 then
+    begin
+      prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right);
+      prerr_endline (CicMetaSubst.ppsubst subst);
+      prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
+      assert false;
+    end;
+*)
+  let ty = apply_subst subst ty in
+  let left = apply_subst subst left in
+  let right = apply_subst subst right in
+  let fix_proof = function
     | NoProof -> NoProof 
-    | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
+    | BasicProof (subst',term) -> BasicProof (subst@subst',term)
     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
 	(*
 	let newsubst = 
           List.map
 	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
+	       let context = apply_subst_context subst context in
+	       let term = apply_subst subst term in
+	       let ty = apply_subst subst ty in  
 		 (i, (context, term, ty))) subst' in *)
           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
     | p -> assert false
@@ -1211,7 +1094,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
diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli
index dd2d4caa1..107e3b819 100644
--- a/components/tactics/paramodulation/inference.mli
+++ b/components/tactics/paramodulation/inference.mli
@@ -25,6 +25,9 @@
 
 val metas_of_proof_time : float ref
 
+(* type substitution = Cic.substitution *)
+type substitution = (int * Cic.term) list 
+
 type equality =
     int *                (* weight *)
     proof *              (* proof *)
@@ -36,9 +39,9 @@ type equality =
 
 and proof =
   | NoProof   (* no proof *)
-  | BasicProof of Cic.term (* already a proof of a goal *)
+  | BasicProof of substitution * Cic.term (* already a proof of a goal *)
   | ProofBlock of (* proof of a rewrite step *)
-      Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
+      substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof
       (* proof of the new meta, proof of the goal from which this comes *)
@@ -53,7 +56,7 @@ val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
 
 val string_of_proof: proof -> string
 
-val filter : Cic.substitution -> Cic.metasenv -> Cic.metasenv
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
 
 exception MatchingFailure
 
@@ -61,7 +64,7 @@ exception MatchingFailure
 val matching:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
@@ -70,7 +73,7 @@ val matching:
 val unification:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
@@ -131,8 +134,12 @@ val is_identity: environment -> equality -> bool
 
 val string_of_equality: ?env:environment -> equality -> string
 
+
 val metas_of_term: Cic.term -> int list
 val metas_of_proof: proof -> int list
 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
+
+val apply_subst: substitution -> Cic.term -> Cic.term
+val ppsubst: substitution -> string
diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d52bf09c3..b902dd86b 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -28,26 +28,10 @@
 open Inference;;
 open Utils;;
 
+let check_table t l =
+  List.fold_left
+    (fun b (_,eq) -> b && (Indexing.in_index t eq)) true l
 
-(*
-for debugging 
-let check_equation env equation msg =
-  let w, proof, (eq_ty, left, right, order), metas = equation in
-  let metasenv, context, ugraph = env in
-  let metasenv' = metasenv @ metas in
-    try
-      CicTypeChecker.type_of_aux' metasenv' context left ugraph;
-      CicTypeChecker.type_of_aux' metasenv' context right ugraph;
-      ()
-    with 
-	CicUtil.Meta_not_found _ as exn ->
-	  begin
-	    prerr_endline msg; 
-	    prerr_endline (CicPp.ppterm left);
-	    prerr_endline (CicPp.ppterm right);
-	    raise exn
-	  end 
-*)
 
 (* set to false to disable paramodulation inside auto_tac *)
 let connect_to_auto = true;;
@@ -91,6 +75,15 @@ let maxmeta = ref 0;;
 let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
+let test eq = false
+(*
+  let (_,(_,_,(ty,left,right,_),m1)) = eq in
+  let actual = 
+    (Inference.metas_of_term left)@(Inference.metas_of_term right) 
+  in
+  let m = List.filter (fun (i, _, _) -> List.mem i actual) m1 in
+    m <> m1
+;; *)
 
 type result =
   | ParamodulationFailure
@@ -337,8 +330,8 @@ let add_to_passive passive (new_neg, new_pos) =
   let ok set equality = not (EqualitySet.mem equality set) in
   let neg = List.filter (ok neg_set) new_neg
   and pos = List.filter (ok pos_set) new_pos in
-  let table =
-    List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+  let table = 
+     List.fold_left (fun tbl e -> Indexing.index tbl e) table pos 
   in
   let add set equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
@@ -621,7 +614,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
     else
       Some (sign, newcurrent)
   in
-  let res =
+  let rec demod current =
     if Utils.debug_metas then
       ignore (Indexing.check_target context current "demod0");
     let res = demodulate active_table current in
@@ -633,8 +626,15 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
     | Some (sign, newcurrent) ->
         match passive_table with
         | None -> res
-        | Some passive_table -> demodulate passive_table newcurrent
-  in
+        | Some passive_table -> 
+	    match demodulate passive_table newcurrent with
+	      | None -> None
+              | Some (sign,newnewcurrent) -> 
+		  if newcurrent <> newnewcurrent then 
+		    demod newnewcurrent
+		  else Some (sign,newnewcurrent)
+  in 
+  let res = demod current in
   match res with
   | None -> None
   | Some (Negative, c) ->
@@ -757,6 +757,60 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
 ;;
 
 
+(** simplifies a goal with equalities in active and passive *)  
+let rec simplify_goal env goal ?passive (active_list, active_table) =
+  let pl, passive_table =
+    match passive with
+    | None -> [], None
+    | Some ((pn, _), (pp, _), pt) ->
+        let pn = List.map (fun e -> (Negative, e)) pn
+        and pp = List.map (fun e -> (Positive, e)) pp in
+        pn @ pp, Some pt
+  in
+
+  let demodulate table goal = 
+    let newmeta, newgoal =
+      Indexing.demodulation_goal !maxmeta env table goal in
+    maxmeta := newmeta;
+    goal <> newgoal, newgoal
+  in
+  let changed, goal =
+    match passive_table with
+    | None -> demodulate active_table goal
+    | Some passive_table ->
+        let changed, goal = demodulate active_table goal in
+        let changed', goal = demodulate passive_table goal in
+        (changed || changed'), goal
+  in
+  changed, if not changed then goal 
+  else snd (simplify_goal env goal ?passive (active_list, active_table))
+;;
+
+
+let simplify_goals env goals ?passive active =
+  let a_goals, p_goals = goals in
+  let p_goals = 
+    List.map
+      (fun (d, gl) ->
+         let gl =
+           List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
+         d, gl)
+      p_goals
+  in
+  let goals =
+    List.fold_left
+      (fun (a, p) (d, gl) ->
+         let changed = ref false in
+         let gl =
+           List.map
+             (fun g ->
+                let c, g = simplify_goal env g ?passive active in
+                changed := !changed || c; g) gl in
+         if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
+      ([], p_goals) a_goals
+  in
+  goals
+;;
 
 
 (** simplifies active usign new *)
@@ -935,60 +989,6 @@ let activate_theorem (active, passive) =
 ;;
 
 
-(** simplifies a goal with equalities in active and passive *)  
-let simplify_goal env goal ?passive (active_list, active_table) =
-  let pl, passive_table =
-    match passive with
-    | None -> [], None
-    | Some ((pn, _), (pp, _), pt) ->
-        let pn = List.map (fun e -> (Negative, e)) pn
-        and pp = List.map (fun e -> (Positive, e)) pp in
-        pn @ pp, Some pt
-  in
-
-  let demodulate table goal = 
-    let newmeta, newgoal =
-      Indexing.demodulation_goal !maxmeta env table goal in
-    maxmeta := newmeta;
-    goal != newgoal, newgoal
-  in
-  let changed, goal =
-    match passive_table with
-    | None -> demodulate active_table goal
-    | Some passive_table ->
-        let changed, goal = demodulate active_table goal in
-        let changed', goal = demodulate passive_table goal in
-        (changed || changed'), goal
-  in
-  changed, goal
-;;
-
-
-let simplify_goals env goals ?passive active =
-  let a_goals, p_goals = goals in
-  let p_goals = 
-    List.map
-      (fun (d, gl) ->
-         let gl =
-           List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
-         d, gl)
-      p_goals
-  in
-  let goals =
-    List.fold_left
-      (fun (a, p) (d, gl) ->
-         let changed = ref false in
-         let gl =
-           List.map
-             (fun g ->
-                let c, g = simplify_goal env g ?passive active in
-                changed := !changed || c; g) gl in
-         if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
-      ([], p_goals) a_goals
-  in
-  goals
-;;
-
 
 let simplify_theorems env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
@@ -1067,6 +1067,7 @@ let simplify_equalities env equalities =
           res
 ;;
 
+(*
 (* applies equality to goal to see if the goal can be closed *)
 let apply_equality_to_goal env equality goal =
   let module C = Cic in
@@ -1083,12 +1084,11 @@ let apply_equality_to_goal env equality goal =
 (*           (string_of_equality equality) (CicPp.ppterm gterm))); *)
   try
     let subst, metasenv', _ =
-      (* let menv = metasenv @ metas @ gmetas in *)
       Inference.unification metas gmetas context eqterm gterm ugraph
     in
     let newproof =
       match proof with
-      | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t)
+      | I.BasicProof (subst',t) -> I.BasicProof (subst@subst',t)
       | I.ProofBlock (s, uri, nt, t, pe, p) ->
           I.ProofBlock (subst @ s, uri, nt, t, pe, p)
       | _ -> assert false
@@ -1097,13 +1097,15 @@ let apply_equality_to_goal env equality goal =
       let rec repl = function
         | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp)
         | I.NoProof -> newproof
-        | I.BasicProof p -> newproof
-        | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p)
+        | I.BasicProof _ -> newproof
+        | I.SubProof (t, i, p) -> 
+	    prerr_endline "SUBPROOF!";
+	    I.SubProof (t, i, repl p)
         | _ -> assert false
       in
       repl gproof
     in
-    true, subst, newgproof
+    true, (subst:Inference.substitution), newgproof
   with CicUnification.UnificationFailure _ ->
     false, [], I.NoProof
 ;;
@@ -1162,9 +1164,9 @@ let apply_to_goal env theorems ?passive active goal =
             let newp =
               let rec repl = function
                 | Inference.ProofGoalBlock (_, gp) ->
-                    Inference.ProofGoalBlock (Inference.BasicProof p, gp)
-                | Inference.NoProof -> Inference.BasicProof p
-                | Inference.BasicProof _ -> Inference.BasicProof p
+                    Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+                | Inference.NoProof -> Inference.BasicProof ([],p)
+                | Inference.BasicProof _ -> Inference.BasicProof ([],p)
                 | Inference.SubProof (t, i, p2) ->
                     Inference.SubProof (t, i, repl p2)
                 | _ -> assert false
@@ -1191,10 +1193,11 @@ let apply_to_goal env theorems ?passive active goal =
                            ProofGoalBlock (sp1, gp sp2)
                        | BasicProof _
                        | NoProof ->
-                           SubProof (p, i, BasicProof (Cic.Meta (i, irl)))
+                           SubProof (p, i, BasicProof ([],Cic.Meta (i, irl)))
                        | ProofSymBlock (s, sp) ->
                            ProofSymBlock (s, gp sp)
                        | ProofBlock (s, u, nt, t, pe, sp) ->
+			   prerr_endline "apply_to_goal!";
                            ProofBlock (s, u, nt, t, pe, gp sp)
                      in gp proof
                    in
@@ -1242,7 +1245,7 @@ let apply_to_goal env theorems ?passive active goal =
     else
       false, [], []
   in
-  if r = true then `Ok (s, l) else aux theorems
+  if r = true then `Ok ((s:Cic.substitution),l) else aux theorems
 ;;
 
 
@@ -1291,13 +1294,13 @@ let rec apply_to_goal_conj env theorems ?passive active (depth, goals) =
     let propagate_subst subst (proof, metas, term) =
       let rec repl = function
         | NoProof -> NoProof 
-        | BasicProof t ->
-            BasicProof (CicMetaSubst.apply_subst subst t)
+        | BasicProof (subst',t) ->
+            BasicProof (subst@subst',t)
         | ProofGoalBlock (p, pb) ->
             let pb' = repl pb in
             ProofGoalBlock (p, pb')
         | SubProof (t, i, p) ->
-            let t' = CicMetaSubst.apply_subst subst t in
+            let t' = Inference.apply_subst subst t in
             let p = repl p in
             SubProof (t', i, p)
         | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
@@ -1579,10 +1582,8 @@ let apply_theorem_to_goals env theorems active goals =
     ok, (a_goals, p_goals)
 ;;
 
-
 (* given-clause algorithm with lazy reduction strategy *)
 let rec given_clause dbd env goals theorems passive active =
-  (* let _,context,_ = env in *)
   let goals = simplify_goals env goals active in
   let ok, goals = activate_goal goals in
   (*   let theorems = simplify_theorems env theorems active in *)
@@ -1738,9 +1739,16 @@ and given_clause_aux dbd env goals theorems passive active =
                   ParamodulationSuccess (proof, env)
           )
 ;;
+*)
+
+let counter = ref 0
 
 (** given-clause algorithm with full reduction strategy *)
 let rec given_clause_fullred dbd env goals theorems passive active =
+(*
+  let table,list = active in
+    assert (check_table list table);
+*)
   let goals = simplify_goals env goals ~passive active in 
   let _,context,_ = env in
   let ok, goals = activate_goal goals in
@@ -1761,16 +1769,58 @@ let rec given_clause_fullred dbd env goals theorems passive active =
 (*            (Printf.sprintf "goal activated:\n%s\n%s\n" *)
 (*               (CicPp.ppterm t) (string_of_proof p))); *)
 (*     in *)
-    let ok, goals =
-      apply_goal_to_theorems dbd env theorems ~passive active goals
-    in
+    let ok, proof =
+      (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
+      let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+      match (fst goals) with
+        | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ 
+	    when left = right && iseq uri -> 
+	    let p =
+              Cic.Appl [Cic.MutConstruct (* reflexivity *)
+			(LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
+	    in
+	    let newp =
+              let rec repl = function
+                | Inference.ProofGoalBlock (_, gp) ->
+                    Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+                | Inference.NoProof -> Inference.BasicProof ([],p)
+                | Inference.BasicProof _ -> Inference.BasicProof ([],p)
+                | Inference.SubProof (t, i, p2) ->
+                    Inference.SubProof (t, i, repl p2)
+                | _ -> assert false
+              in
+              repl proof
+            in true, Some newp
+	| _ -> false, None 
+    in 
     if ok then
-      let proof =
+      (* let proof =
         match (fst goals) with
-        | (_, [proof, _, _])::_ -> Some proof
+        | (_, [proof, m, _])::_ -> 
+	    prerr_endline (CicMetaSubst.ppmetasenv [] m); Some proof
         | _ -> assert false
-      in
+      in *)
       ( prerr_endline "esco qui";
+        let active = 
+	  List.filter test (fst active) in
+	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))
+		 active)))
+	in prerr_endline s;
+        let passive = 
+	  List.filter 
+	    (fun x -> test (1,x))
+	    (let x,y,_ = passive in (fst x)@(fst y)) in
+	let p = Printf.sprintf "passives:\n%s\n"
+	  (String.concat "\n"
+             ((List.map
+		 (fun e -> 
+                    (string_of_equality ~env e))
+		 passive)))
+	in prerr_endline p;
         (*
 	let s = Printf.sprintf "actives:\n%s\n"
 	  (String.concat "\n"
@@ -1806,10 +1856,29 @@ let rec given_clause_fullred dbd env goals theorems passive active =
       else given_clause_fullred_aux dbd env goals theorems passive active
     
 and given_clause_fullred_aux dbd env goals theorems passive active =
-  prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^ 
+  prerr_endline (string_of_int !counter ^ 
+		 " MAXMETA: " ^ string_of_int !maxmeta ^ 
                  " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
 		 " #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"
@@ -1855,11 +1924,20 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
       given_clause_fullred dbd env goals theorems passive active        
   | false ->
       let (sign, current), passive = select env (fst goals) passive active in
-      (* let names = 
-        List.map (HExtlib.map_option (fun (name,_) -> name)) context in *)
-      prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^ 
-                     string_of_equality ~env current);
-		  (* (CicPp.pp (Inference.term_of_equality current) names));*)
+      prerr_endline 
+	("Selected = " ^ (string_of_sign sign) ^ " " ^ 
+	   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 (sign, current) ~passive active in
       let time2 = Unix.gettimeofday () in
@@ -1869,11 +1947,24 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
           (* weight_age_counter := !weight_age_counter + 1; *)
           given_clause_fullred dbd env goals theorems passive active
       | Some (sign, current) ->
+          if test (sign, current) then
+	    (prerr_endline 
+	      ("Simplified = " ^ (string_of_sign sign) ^ " " ^ 
+	     string_of_equality ~env current);
+	     let active = fst active in
+	     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))
+		 active)))
+	     in prerr_endline s;
+               assert false);
           if (sign = Negative) && (is_identity env current) then (
             debug_print
               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                        (string_of_equality ~env current)));
-            let _, proof, _, _ = current in 
+            let _, proof, _, m = current in 
             ParamodulationSuccess (Some proof, env)
           ) else (
             debug_print
@@ -1911,13 +2002,14 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
             in
             let rec simplify new' active passive =
               let t1 = Unix.gettimeofday () in
-              let new' = forward_simplify_new env new' ~passive active 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 =
-                backward_simplify env new' ~passive active in
+                backward_simplify env new' ~passive  active in
+              
               let t2 = Unix.gettimeofday () in
                 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
@@ -1926,20 +2018,20 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               | None, Some (n, p) ->
                   let nn, np = new' in
 		    if Utils.debug_metas then
-		      (List.iter 
-                        (fun x -> ignore 
-                          (Indexing.check_target context x "simplify1"))
-                        n;
-		      List.iter 
-                        (fun x -> ignore 
-                          (Indexing.check_target context x "simplify2"))
-                        p);
-                  simplify (nn @ n, np @ p) active passive
+		      begin
+			List.iter 
+			  (fun x->Indexing.check_target context x "simplify1")
+			  n;
+			List.iter 
+			  (fun x->Indexing.check_target context x "simplify2")
+			  p
+		      end;
+                    simplify (nn @ n, np @ p) active passive
               | Some (n, p), Some (rn, rp) ->
                   let nn, np = new' in
                   simplify (nn @ n @ rn, np @ p @ rp) active passive
             in
-            let active, passive, new' = simplify new' active passive in
+            let active, _, new' = simplify new' active passive in
 (* pessima prova 
 	    let new1 = prova env new' active in
             let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
@@ -2140,7 +2232,7 @@ let main dbd full term metasenv ugraph =
                   (fst theorems)))))
   in
   (*try*)
-    let goal = Inference.BasicProof new_meta_goal, [], goal in
+    let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
     let equalities = simplify_equalities env 
       (equalities@library_equalities) in 
     let active = make_active () in
@@ -2160,7 +2252,7 @@ let main dbd full term metasenv ugraph =
       start_time := Unix.gettimeofday ();
       let res =
         let goals = make_goals goal in
-        (if !use_fullred then given_clause_fullred else given_clause)
+        (if !use_fullred then given_clause_fullred else given_clause_fullred)
           dbd env goals theorems passive active
       in
       let finish = Unix.gettimeofday () in
@@ -2256,7 +2348,7 @@ let reset_refs () =
   Inference.metas_of_proof_time := 0.;
 ;;
 
-let saturate
+let saturate 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
   reset_refs ();
@@ -2268,6 +2360,7 @@ let saturate
   let goal' = goal in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context));
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let new_meta_goal, metasenv, type_of_goal =
     let irl =
@@ -2280,8 +2373,8 @@ let saturate
     ty
   in
   let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in
-  let goal = Inference.BasicProof new_meta_goal, [], goal in
+  let env = (metasenv, context, ugraph) in 
+  let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
@@ -2337,9 +2430,11 @@ let saturate
     (res, finish -. start)
   in
   match res with
-  | ParamodulationSuccess (Some proof, env) ->
+  | ParamodulationSuccess (Some proof, _) ->
       debug_print (lazy "OK, found a proof!");
       let proof = Inference.build_proof_term proof in
+      (* prerr_endline (CicPp.ppterm proof); *)
+      let metasenv = (2839,context,Cic.Rel 17)::(214882,context,Cic.Rel 17)::metasenv in
       let names = names_of_context context in
       let newmetasenv =
         let i1 =
@@ -2539,7 +2634,7 @@ let main_demod_equalities dbd term metasenv ugraph =
   in
   let env = (metasenv, context, ugraph) in
   (*try*)
-    let goal = Inference.BasicProof new_meta_goal, [], goal in
+    let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
     let equalities = simplify_equalities env (equalities@library_equalities) in
     let active = make_active () in
     let passive = make_passive [] equalities in
@@ -2599,7 +2694,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in
   let goalterm = Cic.Meta (metano,irl) in
-  let initgoal = Inference.BasicProof goalterm, [], ty in
+  let initgoal = Inference.BasicProof ([],goalterm), [], ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let equalities = simplify_equalities env (equalities@library_equalities) in   
   let table = 
diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index db19e87d1..16556588f 100644
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -291,7 +291,7 @@ end
 module IntSet = Set.Make(OrderedInt)
 
 let compute_equality_weight (ty,left,right,o) =
-  let factor = 1 in
+  let factor = 2 in
   match o with
     | Lt -> 
 	let w, m = (weight_of_term