X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.mli;h=b1c09277ba989b086d06e07ab091811f19d1c5b1;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=1f0705881994baf0262fffc861e5580b714160a8;hpb=3c9c376401844c389d682ba835845443105e4b1a;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 1f0705881..b1c09277b 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -52,10 +52,8 @@ 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 *) +(* subst_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 +val subst_meta : (Cic.term option) list -> Cic.term -> Cic.term