]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4d602b5) | patch
delifting a Meta with an IRL w.r.t. another IRL completely changed.
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 15 Oct 2008 22:31:41 +0000 (22:31 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 15 Oct 2008 22:31:41 +0000 (22:31 +0000)
commitf31566c556d6c47e283995f50d29f98d509a1fef
tree559530740c2b24aa8419efa67a34d8653e4c14a9tree | snapshot
parent4d602b51da8071c1d21424ec78691c90b2bd2f0ecommit | diff
delifting a Meta with an IRL w.r.t. another IRL completely changed.
the explanation is on my whiteboard, hope someone copies it
helm/software/components/ng_refiner/nCicMetaSubst.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.