(* $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] *)
(* well typed and avoid_beta_redexes is true. *)
val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
-(* psubst [avoid] [delift] [lift_args] [t] [map_arg] [args]
+(* psubst [avoid] [map_arg] [args] [t]
* [avoid] : do not leave newly created beta-redexes, default false
- * [delift] : perform delifting
* [t] : term to fill in
- * [lift_args] : lift argument after map_arg is applied
* [args] : stuff to substitute
* [map_arg] : map the argument to obtain a term
* the function is ReductionStrategy.from_env_for_unwind when psubst is
* used to implement nCicReduction.unwind' *)
val psubst :
- ?avoid_beta_redexes:bool -> bool -> int ->
+ ?avoid_beta_redexes:bool ->
('a -> NCic.term) -> 'a list -> NCic.term ->
NCic.term