- destruct: core of subst tactic implemented,

[helm.git] / components / tactics / proofEngineTypes.mli

diff --git a/components/tactics/proofEngineTypes.mli b/components/tactics/proofEngineTypes.mli
index 6edcfeccc053a7559b715604e9a08f8c421a66f9..7c7b8330ee13d7cf075c6247dd4a293dc9520d16 100644 (file)
--- a/components/tactics/proofEngineTypes.mli
+++ b/components/tactics/proofEngineTypes.mli
@@ -75,3 +75,4 @@ type mk_fresh_name_type =
 
 val goals_of_proof: proof -> goal list
 
+val hole: Cic.term