"..." -> "\ldots" for implicit vectors

[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 f470b8a4de0aea8007da050116203c4192f49231..38408fe13203b10bda43ae7b46c2cde058348fdb 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.mli
+++ b/helm/software/components/ng_kernel/nCicSubstitution.mli
@@ -11,6 +11,12 @@
 
 (* $Id$ *)
 
+val set_ppterm : (context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
+  ?inside_fix:bool ->
+   NCic.term -> string) -> unit
+
 (* lift n t                                                              *)
 (*  lifts [t] of [n]                                                     *)
 (*  [from] default 1, lifts only indexes >= [from]                       *)