alpha equivalence test factorized and moved to CicUtil

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

diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index d80814fc363da2945b236a42381ba67e2e8b03bd..5f8a9a37f91ab400b8574cea9f0afe7e1960f2ea 100644 (file)
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -123,7 +123,7 @@ 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:(CicUtil.alpha_equivalence)
     ~what: (if isSetType
      then (rightparameters_ @ [term] ) 
      else (rightparameters_ ) )
@@ -151,7 +151,7 @@ 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:(CicUtil.alpha_equivalence)
      ~what: (rightparameters_ ) 
      ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
      ~where:termty), (* type of H with replaced right parameters *)