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

diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli
index b032a2218..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
@@ -30,4 +28,5 @@ val map:
  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
  ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term
 
-val is_closed: NCic.term -> bool
+val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
+