]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/theory.ml
This commit was manufactured by cvs2svn to create branch 'helm'.
[helm.git] / helm / interface / theory.ml
diff --git a/helm/interface/theory.ml b/helm/interface/theory.ml
deleted file mode 100644 (file)
index be5b288..0000000
+++ /dev/null
@@ -1,9 +0,0 @@
-type theory_elem =
-   Theorem of string                    (* uri *)
- | Definition of string                 (* uri *)
- | Axiom of string                      (* uri *)
- | Variable of string                   (* uri *)
- | Section of string * theory_elem list (* uri, subtheory *)
-and theory =
- string * theory_elem list              (* uri, subtheory *)
-;;