Corrected a bug relative to the application of substs in the "on goal"

case.

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index b80ac7e9ce7007aa8c83c1da55c8d4a477b9021a..b5f4af9d6f8ede74f3a1508207fba88da6257950 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
-
+              
 let eqsig = ref (fun _ -> assert false);;
 let set_sig f = eqsig:= f;;
 let get_sig = fun x -> !eqsig x;;
@@ -219,6 +219,14 @@ let debug c _ = c;;
     ;;
 
   let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
+    let module NCicBlob = 
+       NCicBlob.NCicBlob(
+        struct
+          let metasenv = [] let subst = [] let context = []
+        end)
+     in
+     let  module Pp = Pp.Pp(NCicBlob) 
+     in
     let module Subst = FoSubst in
     let position i l = 
       let rec aux = function
@@ -261,11 +269,11 @@ let debug c _ = c;;
           let amount = List.length seen in
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
-            let lit = Subst.apply_subst subst lit in
+            let lit = Subst.apply_subst subst lit in 
             let eq_ty = extract amount [] lit in
             let refl = mk_refl eq_ty in
-             (*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
-             (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
+             (* prerr_endline ("Reached m point, id=" ^ (string_of_int id));
+                (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
                 aux true ((id,([],lit))::seen) (id::tl))) *)
               NCicSubstitution.subst 
                 ~avoid_beta_redexes:true ~no_implicit:false refl
@@ -277,8 +285,8 @@ let debug c _ = c;;
               aux ongoal seen tl
           | Terms.Step _ when tl=[] -> assert false
           | Terms.Exact ft ->
-              (* prerr_endline ("Exact for " ^ (string_of_int id));*)
-              (*
+             (*
+               prerr_endline ("Exact for " ^ (string_of_int id));
                NCic.LetIn ("clause_" ^ string_of_int id, 
                  close_with_forall vl (extract amount vl lit),
                  close_with_lambdas vl (extract amount vl ft),
@@ -292,10 +300,12 @@ let debug c _ = c;;
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
           | Terms.Step (_, id1, id2, dir, pos, subst) ->
               let id, id1,(lit,vl,proof) =
-                if ongoal then id1,id,get_literal id1
-                else id,id1,(lit,vl,proof)
-              in
-              let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
+                if ongoal then
+                 let lit,vl,proof = get_literal id1 in
+                 id1,id,(Subst.apply_subst subst lit, 
+                         Subst.filter subst vl, proof)
+                else id,id1,(lit,vl,proof) in
+              let vl = if ongoal then [] else vl in
               let proof_of_id id = 
                 let vars = List.rev (vars_of id seen) in
                 let args = List.map (Subst.apply_subst subst) vars in
@@ -347,12 +357,15 @@ let debug c _ = c;;
                       extract amount vl (Subst.apply_subst subst r)
                   | _ -> assert false
                 in
-                  (*prerr_endline "mk_predicate :";
+                 (*
+                  prerr_endline "mk_predicate :";
                   if ongoal then prerr_endline "ongoal=true"
                   else prerr_endline "ongoal=false";
                   prerr_endline ("id=" ^ string_of_int id);
-                  prerr_endline ("id1=" ^ string_of_int id1);
-                  prerr_endline ("id2=" ^ string_of_int id2);
+                  prerr_endline ("id1=" ^ string_of_int id1 
+                                ^": " ^ Pp.pp_foterm id1_ty);
+                  prerr_endline ("id2=" ^ string_of_int id2
+                                ^ ": " ^ NCicPp.ppterm [][][] id2_ty);
                   prerr_endline ("Positions :" ^
                                    (String.concat ", "
                                       (List.map string_of_int pos)));*)