X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.mli;h=7e27a5d4ceab9cf82b05c9d4259d116a4150e187;hb=c450fdfb1b02eb69e5e7ef25f0acdf80157710df;hp=ad8074dc7fef40a4e0118cc290c3186227bb0f10;hpb=c35e139601a743e7e4b6f4abda745628efdb4744;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli
index ad8074dc7..7e27a5d4c 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.mli
+++ b/helm/software/components/ng_kernel/nCicSubstitution.mli
@@ -17,6 +17,8 @@ val set_ppterm : (context:NCic.context ->
   ?inside_fix:bool ->
    NCic.term -> string) -> unit
 
+val lift_from : ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term 
+
 (* lift n t                                                              *)
 (*  lifts [t] of [n]                                                     *)
 (*  [from] default 1, lifts only indexes >= [from]                       *)