]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2257421) | patch
- mk_restricted_irl removed, the non-optimized code was the same
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 21 Oct 2008 11:33:33 +0000 (11:33 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 21 Oct 2008 11:33:33 +0000 (11:33 +0000)
commite1ffde2ba67b8a2f7d4d97898ba28afd65d96ea7
tree02675d27a6417b47a42752946f2c64a94b328872tree | snapshot
parent22574214f7ab6b0ce7de37b50cad2037074c51b0commit | diff
- mk_restricted_irl removed, the non-optimized code was the same
- delift fixed in case Meta (used to produce negative shift/irl-len)
- fix-sorts takes into account the swap parameter to implement cumulativity
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
Unnamed repository; edit this file 'description' to name the repository.