From a93e4b83ec988ad0b41eb8ea36f127613c12e16b Mon Sep 17 00:00:00 2001
From: =?utf8?q?Michele=20Galat=C3=A0?= <??>
Date: Thu, 29 Aug 2002 13:19:02 +0000
Subject: [PATCH] Type expression simplified.

---
 helm/gTopLevel/proofEngineReduction.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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
-- 
2.39.2