]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b94b62) | patch
Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Fri, 27 Jan 2012 14:31:20 +0000 (14:31 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Fri, 27 Jan 2012 14:31:20 +0000 (14:31 +0000)
commite305a62a7cb0a49fea3d241474e4c5bcd40e7272
tree4055ea031a8eb16419b00e5a937bc7b969063409tree | snapshot
parent5b94b621e536ab79462d2b553868bee281776b57commit | diff
Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
call on its body without applying the local context, resulting in various
assertion failures).
matita/components/ng_refiner/nCicMetaSubst.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.