X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Finversion.ml;h=5f90c45ebbee4854c64ebe0e44c5883d7d1773ea;hb=7c84225a8e472e754f1baf8f8b37f8627c8da6fa;hp=d80814fc363da2945b236a42381ba67e2e8b03bd;hpb=e00d05ab58597620345c2fd49b84a23efa8db34c;p=helm.git

diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index d80814fc3..5f90c45eb 100644
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -123,7 +123,8 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty
      (CicSubstitution.lift 1 termty)
      isSetType (CicSubstitution.lift 1 term))
    | [] -> ProofEngineReduction.replace_lifting 
-    ~equality:(ProofEngineReduction.alpha_equivalence)
+    ~equality:(fun _ -> CicUtil.alpha_equivalence)
+    ~context:[]
     ~what: (if isSetType
      then (rightparameters_ @ [term] ) 
      else (rightparameters_ ) )
@@ -151,7 +152,8 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_
    | [] when isSetType -> Cic.Lambda (
     (Cic.Name ("lambda" ^ (string_of_int nright))),
     (ProofEngineReduction.replace_lifting
-     ~equality:(ProofEngineReduction.alpha_equivalence)
+     ~equality:(fun _ -> CicUtil.alpha_equivalence)
+     ~context:[]
      ~what: (rightparameters_ ) 
      ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
      ~where:termty), (* type of H with replaced right parameters *)