X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicSubstitution.mli;h=36291fb184b284971cf8e81c36cb1aaf09fc124d;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=21a1f5d0e579d775c9e1ea2117b56898506f1990;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_proof_checking/cicSubstitution.mli b/components/cic_proof_checking/cicSubstitution.mli
index 21a1f5d0e..36291fb18 100644
--- a/components/cic_proof_checking/cicSubstitution.mli
+++ b/components/cic_proof_checking/cicSubstitution.mli
@@ -40,9 +40,12 @@ val lift : int -> Cic.term -> Cic.term
 (* as lift but lifts only indexes >= from *)
 val lift_from: int -> int -> Cic.term -> Cic.term
 
-(* subst t1 t2                          *)
-(* substitutes [t1] for [Rel 1] in [t2] *)
-val subst : Cic.term -> Cic.term -> Cic.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 -> Cic.term -> Cic.term -> Cic.term
 
 (* subst_vars exp_named_subst t2     *)
 (* applies [exp_named_subst] to [t2] *)