This commit was manufactured by cvs2svn to create branch

[helm.git] / helm / ocaml / tactics / ring.mli

diff --git a/helm/ocaml/tactics/ring.mli b/helm/ocaml/tactics/ring.mli
deleted file mode 100644 (file)
index b6eb34b..0000000
--- a/helm/ocaml/tactics/ring.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-
-  (* ring tactics *)
-val ring_tac: ProofEngineTypes.tactic
-
-(*Galla: spostata in variuosTactics.ml
-  (* auxiliary tactics *)
-val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
-*)
-
-(* spostata in variousTactics.ml
-val reflexivity_tac: ProofEngineTypes.tactic
-*)