...

[helm.git] / helm / software / components / cic_proof_checking / cicSubstitution.mli

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.mli b/helm/software/components/cic_proof_checking/cicSubstitution.mli
index 21a1f5d0e579d775c9e1ea2117b56898506f1990..68311c68c0f6d4919be1848bab8de11e49ce17be 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicSubstitution.mli
+++ b/helm/software/components/cic_proof_checking/cicSubstitution.mli
@@ -35,14 +35,22 @@ exception ReferenceToInductiveDefinition;;
 (* since it needs to restrict the metavariables in case of failure      *)
 val lift : int -> Cic.term -> Cic.term
 
-
 (* lift from n t *)
 (* 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
+(* lift map t *)
+(* as lift_from but lifts indexes by applying a map to them
+   the first argument of the map is the current depth *)
+(* FG: this is used in CicDischarge to perform non-linear relocation *)
+val lift_map: int -> (int -> int -> int) -> 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] *)