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

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

diff --git a/helm/interface/cicReduction.mli b/helm/interface/cicReduction.mli
deleted file mode 100644 (file)
index bcc91b0..0000000
--- a/helm/interface/cicReduction.mli
+++ /dev/null
@@ -1,9 +0,0 @@
-exception WrongUriToInductiveDefinition
-exception ReferenceToDefinition
-exception ReferenceToAxiom
-exception ReferenceToVariable
-exception ReferenceToCurrentProof
-exception ReferenceToInductiveDefinition
-val fdebug : int ref
-val whd : Cic.term -> Cic.term
-val are_convertible : Cic.term -> Cic.term -> bool