]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f3cddcf) | patch
improved check in delift for flexible lc entries.
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Sep 2009 13:53:04 +0000 (13:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Sep 2009 13:53:04 +0000 (13:53 +0000)
commit8049c166a37789d7a1b1ca1c3a1174712bbf87ba
tree56f9e4603e7e865222f78617de2ed6d437bc4edbtree | snapshot
parentf3cddcf163b36101158ea33b3fad368ac8c62d75commit | diff
improved check in delift for flexible lc entries.
added a function to easily delift a term w.r.t.
other terms, thanks to delift, used to propagate the expected type
of a letin.
helm/software/components/ng_refiner/nCicMetaSubst.ml diff | blob | history
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnification.mli diff | blob | history
helm/software/matita/nlibrary/depends diff | blob | history
helm/software/matita/nlibrary/depends.dot diff | blob | history
helm/software/matita/nlibrary/depends.png diff | blob | history
helm/software/matita/nlibrary/sets/partitions.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.