- Procedural convertible rewrites in the conclusion are now detected and replaced...

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.mli

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli
index 03faf269bf136490099d05936b3ac24963b9d05d..c021c7c69e8a768d09cc44c9c4524bb9001b5e92 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.mli
+++ b/helm/software/components/acic_procedural/proceduralHelpers.mli
@@ -99,5 +99,5 @@ val is_acic_proof:
    (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm ->
    bool
 
-val alpha_equivalence:
+val alpha:
    ?flatten:bool -> Cic.context -> Cic.term -> Cic.term -> bool