parameter sintax added to axiom statement

[helm.git] / helm / software / components / ng_kernel / nCicSubstitution.mli

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli
index ad8074dc7fef40a4e0118cc290c3186227bb0f10..7e27a5d4ceab9cf82b05c9d4259d116a4150e187 100644 (file)
--- 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]                       *)