X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=57c440860a78dc3016ba1b3c11917861d9b13a5b;hb=8c89e28033f817fce728ea7def1c2c13ae040d31;hp=c31538bda7595dd0b223311d8ee2bc7049dfd262;hpb=356f9fafa095801f1be70ff495f0977ce96ed6bc;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index c31538bda..57c440860 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -422,8 +422,11 @@ let build_proof_step lift subst p1 p2 pos l r pred =
         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
 ;;
 
-let parametrize_proof p ty = 
-  let parameters = CicUtil.metas_of_term p in (* ?if they are under a lambda? *)
+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 = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
@@ -434,7 +437,7 @@ let parametrize_proof p ty =
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what ~with_what ~where:p
+    ~equality:(fun t1 t2 -> match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) ~what ~with_what ~where:p
   in
   let ty_of_m _ = ty (*function 
     | Cic.Meta (i,_) -> List.assoc i menv 
@@ -502,17 +505,19 @@ let get_duplicate_step_in_wfo l p =
   let add i n = 
     let p,_,_ = proof_of_id i in 
     match p with 
-    | Exact _ -> ()
+    | Exact _ -> true
     | _ -> 
-        try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1)
-        with Not_found -> Hashtbl.add h i (n,1)
+        try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1);false
+        with Not_found -> Hashtbl.add h i (n,1);true
   in
   let rec aux n = function
     | Exact _ -> n
     | Step (_,(_,i1,(_,i2),_)) -> 
-        add i1 n;add i2 n;
-        max (aux (n+1) (let p,_,_ = proof_of_id i1 in p))
-          (aux (n+1) (let p,_,_ = proof_of_id i2 in p))
+	let go_on_1 = add i1 n in
+	let go_on_2 = add i2 n in
+        max 
+         (if go_on_1 then aux (n+1) (let p,_,_ = proof_of_id i1 in p) else n+1)
+         (if go_on_2 then aux (n+1) (let p,_,_ = proof_of_id i2 in p) else n+1)
   in
   let i = aux 0 p in 
   let _ = 
@@ -537,9 +542,6 @@ let build_proof_term h lift proof =
   let rec aux = function
      | Exact term -> CicSubstitution.lift lift term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
-         if Subst.is_in_subst 9 subst then
-           prerr_endline (Printf.sprintf "ID %d-%d has: %s\n" id1 id2 (Subst.ppsubst
-           subst));
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
            build_proof_step lift subst p1 p2 pos l r pred
@@ -557,10 +559,10 @@ let build_goal_proof l initial ty se =
   let lets,_,h = 
     List.fold_left
       (fun (acc,n,h) id -> 
-        let p,_,_ = proof_of_id id in
+        let p,l,r = proof_of_id id in
         let cic = build_proof_term h n p in
         let real_cic,instance = 
-          parametrize_proof cic (CicSubstitution.lift n mty)
+          parametrize_proof cic l r (CicSubstitution.lift n mty)
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h)