X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=64f2faa7d796cb2d25fc84e4a0e6f5e9d93b836d;hb=246f3c2f2d26655129efacf830ecff47094795b4;hp=bfbab9c3ec43c878a9f4f08be05dbeab1f26acd0;hpb=8cbaf41588bb862705690b37aa856b6505611274;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bfbab9c3e..64f2faa7d 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -786,10 +786,11 @@ let build_proof_term bag eq h lift proof =
    aux proof
 ;;
 
-let build_goal_proof bag eq l initial ty se context menv =
+let build_goal_proof ?(contextualize=true) ?(forward=false) bag eq l initial ty se context menv =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo bag l initial in
   let letsno = List.length lets in
+  let l = if forward then List.rev l else l in
   let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
   let lets,_,h = 
     List.fold_left
@@ -812,7 +813,8 @@ let build_goal_proof bag eq l initial ty se context menv =
       | (rule,pos,id,subst,pred)::tl ->
           let p,l,r = proof_of_id bag id in
            let p = build_proof_term bag eq h letsno p in
-           let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+           let pos = if forward then pos else
+	       if pos = Utils.Left then Utils.Right else Utils.Left in
          let varname = 
            match rule with
            | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos) 
@@ -845,10 +847,11 @@ let build_goal_proof bag eq l initial ty se context menv =
           p))
     lets (letsno-1,initial)
   in
-   canonical 
-     (contextualize_rewrites proof (CicSubstitution.lift letsno ty))
-     context menv,
-   se 
+  let proof = 
+    if contextualize 
+    then contextualize_rewrites proof (CicSubstitution.lift letsno ty)
+    else proof in
+  canonical proof context menv, se
 ;;
 
 let refl_proof eq_uri ty term = 
@@ -885,10 +888,12 @@ let relocate newmeta menv to_be_relocated =
         let irl = [] in
         let newmeta = Cic.Meta(maxmeta,irl) in
         let newsubst = Subst.buildsubst i context newmeta ty subst in
-        newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) 
+        (* newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) *)
+        newsubst, (maxmeta,[],ty)::metasenv, maxmeta+1) 
       to_be_relocated (Subst.empty_subst, [], newmeta+1)
   in
-  let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
+  (* let subst = Subst.flatten_subst subst in *)
+  let menv = Subst.apply_subst_metasenv subst (menv @ newmetasenv) in
   subst, menv, newmeta
 
 let fix_metas_goal newmeta goal =
@@ -909,11 +914,13 @@ let fix_metas_goal newmeta goal =
 let fix_metas bag newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
-(* List.map (fun i ,_,_ -> i) menv *)
+  List.map (fun i ,_,_ -> i) menv 
+(*
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
          (Utils.metas_of_term left @ Utils.metas_of_term right @
          Utils.metas_of_term ty)) 
+*)
   in
   let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in