X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUtils.mli;h=6baaeda03c61abcaeacfdd8673b6a0440ddbfe5e;hb=dcdbb979433a61e2ef2842d96604098728824416;hp=e010f5d19b443cdddef76b5ec575839679430223;hpb=d66222777ea069f6cde311548dc327f5be09ec59;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli
index e010f5d19..6baaeda03 100644
--- a/helm/software/components/ng_kernel/nCicUtils.mli
+++ b/helm/software/components/ng_kernel/nCicUtils.mli
@@ -9,13 +9,11 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-(* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *)
+(* $Id$ *)
 
 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
+