(* $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] *)