]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: de016fe) | patch
3 nasty bugs fixed:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 6 Oct 2008 15:02:12 +0000 (15:02 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 6 Oct 2008 15:02:12 +0000 (15:02 +0000)
commit7d470885cbbe8c7c102c390eef61e26bff1686c0
tree4a51e28ff2a97e52ab083671d1e8b85e5afe26batree | snapshot
parentde016fec107170e4eb692b41c36a88cdc805b60acommit | diff
3 nasty bugs fixed:

- mk_restricted_irl has been duplicated
  - mk_restricted_irl generates an irl
  - mk_perforated_irl generates a restricted local context suitable for a new meta

- a wrong optimization in psubst was lifting of a bad amount

- force_does_not_occurr was not delifting rels to hypotheses to be cancelled
helm/software/components/ng_refiner/.depend.opt diff | blob | history
helm/software/components/ng_refiner/check.ml diff | blob | history
helm/software/components/ng_refiner/esempio.ma diff | blob | history
helm/software/components/ng_refiner/nCicMetaSubst.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.