Initial revision

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

diff --git a/helm/gTopLevel/proofEngineStructuralRules.mli b/helm/gTopLevel/proofEngineStructuralRules.mli
index a0a423cffb6737509e81d4d2abe02dc0a9a6757e..f6ee6a529ec4df3e622447c82822a63d536c986c 100644 (file)
--- 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