debian release 0.0.4-2:

[helm.git] / helm / gTopLevel / proofEngineReduction.mli

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index 3dea540d587e98d04f8ea7858ba04d1c2ed519a0..aa0a3a6489394056178b20314c04162bc816efbe 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -34,10 +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 reduce :
-  (Cic.name * Cic.context_entry) option list -> 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