]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86dbca4) | patch
- delift_type_wrt_term fixed in many ways
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 1 Oct 2009 15:04:27 +0000 (15:04 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 1 Oct 2009 15:04:27 +0000 (15:04 +0000)
commitbb7f9a362891d4377011783016b74f0b0b2a5974
tree8e5715475cd9936dcb7dfa970b6aa36ca9d2c8a2tree | snapshot
parent86dbca4f0bfda375bdf036ec5ce3bf44678415f2commit | diff
- delift_type_wrt_term fixed in many ways
  - as a side effect let in expty propagation works
  - as a side effect lambda_intros now works
- is_flexible (delift) improved in case: (? args) ---subst---> (\lambda .?) args
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
Unnamed repository; edit this file 'description' to name the repository.