?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] *)
(* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *)
(* since it needs to restrict the metavariables in case of failure *)
-val lift : ?from:int -> int -> NCic.term -> NCic.term
+val lift : ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
(* are generated. WARNING: the substitution can diverge when t2 is not *)
(* well typed and avoid_beta_redexes is true. *)
-val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
+val subst :
+ ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
+ NCic.term -> NCic.term -> NCic.term
(* psubst [avoid] [map_arg] [args] [t]
* [avoid] : do not leave newly created beta-redexes, default false
* the function is ReductionStrategy.from_env_for_unwind when psubst is
* used to implement nCicReduction.unwind' *)
val psubst :
- ?avoid_beta_redexes:bool ->
+ ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
('a -> NCic.term) -> 'a list -> NCic.term ->
NCic.term