This commit was manufactured by cvs2svn to create branch 'helm'.

[helm.git] / helm / interface / cicCooking.mli

diff --git a/helm/interface/cicCooking.mli b/helm/interface/cicCooking.mli
deleted file mode 100644 (file)
index 586e5d7..0000000
--- a/helm/interface/cicCooking.mli
+++ /dev/null
@@ -1,6 +0,0 @@
-exception Impossible
-exception NotImplemented of int * string
-exception WrongUriToConstant
-exception WrongUriToVariable of string
-exception WrongUriToInductiveDefinition
-val cook_obj : Cic.obj -> UriManager.uri -> (int * Cic.obj) list