Initial revision

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

diff --git a/helm/interface/cicReduction.mli b/helm/interface/cicReduction.mli
new file mode 100644 (file)
index 0000000..bcc91b0
--- /dev/null
+++ b/helm/interface/cicReduction.mli
@@ -0,0 +1,9 @@
+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