]> matita.cs.unibo.it Git - helm.git/commit
update in delayed_updating
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 9 May 2022 19:08:36 +0000 (21:08 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 9 May 2022 19:08:36 +0000 (21:08 +0200)
commitd59f1c74c62ad3706d50707bb68758d88fbed006
treeca5ad209a397867b99b4f03e6349e7ec6324a2ba
parent8c6e4521acc9dad59b3ceebae66ce5e7a63a7c44
update in delayed_updating

+ main function to locate the referred binder
+ update function for unfold
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/downarrowright_2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/power_2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail_depth.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma [new file with mode: 0644]
matita/matita/predefined_virtuals.ml