Unfolded exact letins during proof reconstruction.

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 1c74ac9e5b259d74fef23108a89aee864f88fb41..bc4b5bfcdd9f2b7c53691f1bdb11847ad5cef036 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -173,9 +173,12 @@ let debug c _ = c;;
            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,
-                aux true ((id,([],lit))::seen) (id::tl)))
+             (*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
+                (aux true ((id,([],lit))::seen) (id::tl))
           else
           match proof with
           | Terms.Exact _ when tl=[] ->
@@ -184,11 +187,18 @@ let debug c _ = c;;
           | Terms.Step _ when tl=[] -> assert false
           | Terms.Exact ft ->
              (* 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),
                  aux ongoal 
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+             *)
+               NCicSubstitution.subst 
+                ~avoid_beta_redexes:true ~no_implicit:false
+                (close_with_lambdas vl (extract amount vl ft))
+                 (aux ongoal 
+                   ((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