1) The NG kernel now accepts only usage of declared universes

[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 11eca58c02f6fa0b0ab91a3baf2a7afdb859b968..6baaeda03c61abcaeacfdd8673b6a0440ddbfe5e 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUtils.mli
+++ b/helm/software/components/ng_kernel/nCicUtils.mli
@@ -14,8 +14,6 @@
 exception Subst_not_found of int
 exception Meta_not_found of int
 
-val sharing_map: ('a -> 'a) -> 'a list -> 'a list
-
 val expand_local_context : NCic.lc_kind -> NCic.term list
 
 val lookup_subst: int ->  NCic.substitution -> NCic.subst_entry
@@ -29,3 +27,6 @@ val fold:
 val map:
  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
  ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term
+
+val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
+