]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cbe0302) | patch
Fixed an hidden occur check problem: when a Meta is being delifted,
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 12 Nov 2004 18:13:17 +0000 (18:13 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 12 Nov 2004 18:13:17 +0000 (18:13 +0000)
commit9369ab9136d5726669b30f3598f2e433fba438d9
treea5aeb2dc767809ce4bb1e3ba8c0f1ba30d773a12tree | snapshot
parentcbe0302d6b0d2bca6657fa7479a62d0004665612commit | diff
Fixed an hidden occur check problem: when a Meta is being delifted,
apply substitution on the fly and delift the result. Previously we did
not recursively check the instantiation of the Meta.
helm/ocaml/cic_unification/cicMetaSubst.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.