X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineStructuralRules.mli;h=f6ee6a529ec4df3e622447c82822a63d536c986c;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=a0a423cffb6737509e81d4d2abe02dc0a9a6757e;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git

diff --git a/helm/gTopLevel/proofEngineStructuralRules.mli b/helm/gTopLevel/proofEngineStructuralRules.mli
index a0a423cff..f6ee6a529 100644
--- a/helm/gTopLevel/proofEngineStructuralRules.mli
+++ b/helm/gTopLevel/proofEngineStructuralRules.mli
@@ -1,6 +1,2 @@
-val clearbody:
-  status: ProofEngineTypes.status ->
-  hyp: Cic.hypothesis -> ProofEngineTypes.status
-val clear:
-  status: ProofEngineTypes.status ->
-  hyp: Cic.hypothesis -> ProofEngineTypes.status
+val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
+val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic