X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.mli;h=f185dd6638d9a3eaf30bf078039d1cadbf40d207;hb=8b9c9eae1f9da8908ede64b37f04bb7d9e476f7a;hp=06a7f2b9a171b5f10c3b6953a84e66ded811343b;hpb=a93e4b83ec988ad0b41eb8ea36f127613c12e16b;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index 06a7f2b9a..f185dd663 100644
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -24,8 +24,7 @@
  *)
 
 exception Impossible of int
-exception ReferenceToDefinition
-exception ReferenceToAxiom
+exception ReferenceToConstant
 exception ReferenceToVariable
 exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
@@ -34,9 +33,12 @@ exception RelToHiddenHypothesis
 exception WrongShape
 exception AlreadySimplified
 
-val syntactic_equality : Cic.term -> Cic.term -> bool
+val alpha_equivalence: 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 -> 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