alpha equivalence test factorized and moved to CicUtil

[helm.git] / components / tactics / proofEngineReduction.mli

diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli
index 78f4b7f4c4e8024550fa91dd05a8ae91db2356a6..2d04d39596ea4149042189b2187ffb1245928ebd 100644 (file)
--- a/components/tactics/proofEngineReduction.mli
+++ b/components/tactics/proofEngineReduction.mli
@@ -34,8 +34,6 @@ exception WrongShape
 exception AlreadySimplified
 exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
-val alpha_equivalence: Cic.term -> Cic.term -> bool
-
 (* Replaces "textually" in "where" every term in "what" with the corresponding
    term in "with_what". The terms in "what" ARE NOT lifted when binders are
    crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.