added a CSC's TODO comment

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 2032869911d35fa6154298b7c1bb10d1fa77dff0..3aff92f96c7cf0b2b6c79d1ec688049f3752394a 100644 (file)
--- 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
+