From 42e022596d00f85eebb19b8f7c9029273ad15db1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 27 Jan 2010 09:04:31 +0000 Subject: [PATCH] Unfolded exact letins during proof reconstruction. --- .../components/ng_paramodulation/nCicProof.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) 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 -- 2.39.2