Initial revision

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

diff --git a/helm/interface/cicSubstitution.mli b/helm/interface/cicSubstitution.mli
new file mode 100644 (file)
index 0000000..f83cf05
--- /dev/null
+++ b/helm/interface/cicSubstitution.mli
@@ -0,0 +1,3 @@
+val lift : int -> Cic.term -> Cic.term
+val subst : Cic.term -> Cic.term -> Cic.term
+val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj