simplify has a brand new semantics!

[helm.git] / helm / software / components / tactics / inversion.ml

diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml
index 5f8a9a37f91ab400b8574cea9f0afe7e1960f2ea..5f90c45ebbee4854c64ebe0e44c5883d7d1773ea 100644 (file)
--- a/helm/software/components/tactics/inversion.ml
+++ b/helm/software/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:(CicUtil.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:(CicUtil.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 *)