more cases of the type checker honoured, still missing Match and Const.

[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 7a9ce090b8cd11773bd6492cea234e6d3f9eb2fc..f7bf459188649f758f1f6fc50ed08cdfc2f09648 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUtils.mli
+++ b/helm/software/components/ng_kernel/nCicUtils.mli
@@ -26,10 +26,12 @@
 (* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *)
 
 exception Subst_not_found of int
+exception Meta_not_found of int
 
 val expand_local_context : NCic.lc_kind -> NCic.term list
 
 val lookup_subst: int ->  NCic.substitution -> NCic.subst_entry
+val lookup_meta: int ->  NCic.metasenv -> NCic.conjecture
 
 (* both Meta agnostic, map attempts to preserve sharing.
  * call the 'a->'a function when a binder is crossed *)