New management of resulting subst in deep_eq: used to be malformed.

[helm.git] / matitaB / components / ng_paramodulation / nCicProof.ml

diff --git a/matitaB/components/ng_paramodulation/nCicProof.ml b/matitaB/components/ng_paramodulation/nCicProof.ml
index 50c25315f91bd7ab1758892c857d6d7c6b854fde..5f8ed1733ccfd44888287e0affc9a6b380a923a1 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicProof.ml
+++ b/matitaB/components/ng_paramodulation/nCicProof.ml
@@ -231,24 +231,7 @@ let debug c _ = c;;
       let lit = Subst.apply_subst subst lit in
         extract status 0 [] lit in
     (* composition of all subst acting on goal *)
-    let res_subst =
-      let rec rsaux ongoal acc = 
-       function
-         | [] -> acc (* is the final subst for refl *)
-         | id::tl when ongoal ->
-            let lit,vl,proof = get_literal id in
-             (match proof with
-               | Terms.Exact _ -> rsaux ongoal acc tl
-               | Terms.Step (_, _, _, _, _, s) ->
-                   rsaux ongoal (s@acc) tl)
-         | id::tl -> 
-           (* subst is the the substitution for refl *)
-           rsaux (id=mp) subst tl
-      in 
-      let r = rsaux false [] steps in
-       (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
-           prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
-      r
+    let res_subst = subst 
     in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1