matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
	Thu, 3 May 2018 20:27:36 +0000 (22:27 +0200)
committer	Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
	Thu, 3 May 2018 20:27:36 +0000 (22:27 +0200)
commit	2976c347e18717e691825ebdf73a5ce941c57d1b
tree	4c626df09c899f708aeaa71b080c95ee70d5ed45	tree \| snapshot
parent	a77d0bd6a04e94f765d329d47b37d9e04d349b14	commit \| diff

update in ground_2 and models

+ bug fixed in local environment interpretation
extensional equality of evaluations allows to prove a lemma

17 files changed:

matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/veq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/lib/exteq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/notation/relations/doteq_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.