- init_cache_and_tables rewritten using the automation_cache

[helm.git] / helm / software / components / tactics / proofEngineReduction.mli

diff --git a/helm/software/components/tactics/proofEngineReduction.mli b/helm/software/components/tactics/proofEngineReduction.mli
index f8cdec89b74956f8e01bcef6bdbddb7529047ae2..5bc5f24585326b82d08bc31a17ff3782065abe17 100644 (file)
--- a/helm/software/components/tactics/proofEngineReduction.mli
+++ b/helm/software/components/tactics/proofEngineReduction.mli
@@ -69,6 +69,5 @@ val replace_lifting_csc :
 val replace_with_rel_1_from :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> int -> Cic.term -> Cic.term
-val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term
 val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term