Added Decompose tactic

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

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index ab1b0285e978ce81cd2e762f0dea22562c7c189e..0263fd1e7c31e8e07fb5bc23335905fb051ba1cd 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -81,7 +81,7 @@ val generalize : Cic.term -> unit
 val absurd : Cic.term -> unit
 val contradiction : unit -> unit
 
-val decompose : clist:(Cic.term list) -> unit
+val decompose : Cic.term -> unit
 
 (*
 val decide_equality : unit -> unit