X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.mli;h=aa0a3a6489394056178b20314c04162bc816efbe;hb=c7eb56246dc1199f098ed6c8c77aa08fea9a62f8;hp=e2d96f40b9d64e6a25ed914c6d031ea9600cfaf3;hpb=5dac9432fa233251332953770319c0b95984e1c5;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index e2d96f40b..aa0a3a648 100644
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -34,12 +34,12 @@ exception RelToHiddenHypothesis
 exception WrongShape
 exception AlreadySimplified
 
-val syntactic_equality : Cic.term -> Cic.term -> bool
+val syntactic_equality : alpha_equivalence:bool -> Cic.term -> Cic.term -> bool
 val replace :
   equality:(Cic.term -> 'a -> bool) ->
   what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val replace_lifting :
-  equality:(Cic.term -> 'a -> bool) ->
-  what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
+  equality:(Cic.term -> Cic.term -> bool) ->
+  what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term