]> matita.cs.unibo.it Git - helm.git/commit
CicSubstitution.delift ==> CicMetaSubst.delift_rels
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 9 Jun 2005 15:04:49 +0000 (15:04 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 9 Jun 2005 15:04:49 +0000 (15:04 +0000)
commit17cc9a1c6353a5a57562434e9938fb54ca78b9c6
tree0847ca9576d15a050b3e1e9987ab74b178fc7152
parent4f576c9474396e214db9fcf8bb974c603c16a825
CicSubstitution.delift ==> CicMetaSubst.delift_rels
(since it will need to restrict metavariables in case of Rel capture)
helm/ocaml/cic_proof_checking/cicSubstitution.ml
helm/ocaml/cic_proof_checking/cicSubstitution.mli
helm/ocaml/cic_unification/cicMetaSubst.ml
helm/ocaml/cic_unification/cicMetaSubst.mli
helm/ocaml/cic_unification/cicRefine.ml