Bad hack to avoid failure of conversion (unfolding) in "unfold t in H" where

[helm.git] / helm / software / components / ng_kernel / nCicUtils.mli

diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli
index 45c444ac4118dc926ef1e7b466493fcd4c330f37..6af6ac8f0cc1a7397b4d55b274588b0c5865538a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUtils.mli
+++ b/helm/software/components/ng_kernel/nCicUtils.mli
@@ -25,5 +25,9 @@
 
 (* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *)
 
+exception Subst_not_found of int
+
 val expand_local_context : NCic.lc_kind -> NCic.term list
 
+val lookup_subst: int ->  NCic.substitution -> NCic.subst_entry
+