X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.mli;h=3aff92f96c7cf0b2b6c79d1ec688049f3752394a;hb=bb236c2ac110124de92fa2d0fb2882d273a7f7eb;hp=2032869911d35fa6154298b7c1bb10d1fa77dff0;hpb=9ea87248101d774e1b4c4b706d8d99444b2e5907;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 203286991..3aff92f96 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -42,7 +42,10 @@ val subst : Cic.term -> Cic.term -> Cic.term
 val subst_vars :
  Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term
 
+(* TODO CSC rename to subst_meta *)
+
 (* lift_meta [t_1 ; ... ; t_n] t                                *)
 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
 (* [t_i] is lifted as usual when it crosses an abstraction      *)
 val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term
+