X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.mli;h=06a7f2b9a171b5f10c3b6953a84e66ded811343b;hb=6e08ee8f963bfd73e271737154baf97240bd18c5;hp=3dea540d587e98d04f8ea7858ba04d1c2ed519a0;hpb=4720c6af414c4a834a994fdb404fda2d0c04fc03;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index 3dea540d5..06a7f2b9a 100644
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -38,6 +38,5 @@ val syntactic_equality : 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 reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term