From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 27 Jan 2010 09:04:31 +0000 (+0000)
Subject: Unfolded exact letins during proof reconstruction.
X-Git-Tag: make_still_working~3090
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=42e022596d00f85eebb19b8f7c9029273ad15db1;p=helm.git

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 1c74ac9e5..bc4b5bfcd 100644
--- 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