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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 4 Oct 2014 20:42:40 +0000 (20:42 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 4 Oct 2014 20:42:40 +0000 (20:42 +0000)
commit	9afdb35b870c15760f482a1b4a0ad7b4dcd5172b
tree	dd84e9dc3550a0a908291175371c178bba68b255	tree \| snapshot
parent	6f1f9e20aa2775d41bba64289fc903e6612baaf3	commit \| diff

- nnAuto: we catch TypeCheckerFailure generated at the end of
smart_apply (rel out of context) during equational reasoning,
and we treat it as an Error. TO BE UNDERSTTOD
(this TypeCheckerFailure dramatically interferes with automatic
proof search in \lambda\delta)
- lambdadelta: new definition of fpbg without fpbc + some refactoring

51 files changed:

matita/components/ng_tactics/nnAuto.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpb.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbc.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbc_fleq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fleq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbg.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_fpbs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbg_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/fpbs_fpbc.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbc/lazybtpredproper_8.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/btpredstarproper_8.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_fleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml		diff \| blob \| history

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

RSS Atom