X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=d9e16a255e362ed58d5592e1c9fe33e491e7f22a;hb=4e0ce221e8f218bbf60885173d61ea6ff9324213;hp=fcb4586cb4d8b2e0ecb2e1831797f11a2ef49605;hpb=f809c7537eda20a275b17bc1407f0ee446f70356;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index fcb4586cb..d9e16a255 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -371,12 +371,12 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
   
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
-    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+  ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
 ;;
 
 let put_in_ctx ctx t = 
   ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+  ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
 ;;
 
 let mk_eq uri ty l r =
@@ -581,8 +581,9 @@ let parametrize_proof p l r =
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(fun t1 t2 -> 
+    ~equality:(fun _ t1 t2 -> 
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
+    ~context:[]
     ~what ~with_what ~where:p
   in
   let ty_of_m _ = Cic.Implicit (Some `Type) in