From 142d7ec20150166eb919cabece457375e8813804 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 19 Jan 2004 11:41:56 +0000 Subject: [PATCH] added a CSC's TODO comment --- helm/ocaml/cic_proof_checking/cicSubstitution.mli | 3 +++ 1 file changed, 3 insertions(+) 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 + -- 2.39.2