- added Ring tactic on reals

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

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
new file mode 100644 (file)
index 0000000..87142b5
--- /dev/null
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -0,0 +1,13 @@
+val apply_tac:
+  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+val exact_tac:
+  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+val intros_tac:
+  status: ProofEngineTypes.status -> name: string-> ProofEngineTypes.status
+val cut_tac:
+  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+val letin_tac:
+  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+
+val elim_intros_simpl_tac:
+  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status