]> matita.cs.unibo.it Git - helm.git/commit
the refiner was not checking that the resulting type
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 10 Sep 2009 10:10:10 +0000 (10:10 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 10 Sep 2009 10:10:10 +0000 (10:10 +0000)
commitc1f12859e933fdbd2ca5e054fc23c01f79f8cc56
tree4ac10a74ff2a4e7b213356a70b4c481a34343c50
parentaff007d80f87128884c96a664bc88aec69107d85
the refiner was not checking that the resulting type
of an application was the expected one in case
the application is ((lambda...) ?...) when ?...
resolves to the empty ? vector.
helm/software/components/ng_refiner/nCicCoercion.ml
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_tactics/nTactics.ml