From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 19 Jan 2004 11:41:56 +0000 (+0000)
Subject: added a CSC's TODO comment
X-Git-Tag: V_0_5_1_3~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=142d7ec20150166eb919cabece457375e8813804;p=helm.git

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 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
+