simplify telescope-based notations

These type annotations are no longer needed once we have a bidirectionality hint on tele_app.

Requires stdpp!342 (merged) and !763 (merged).

added S-draft label

mentioned in merge request stdpp!342 (merged)

added 4 commits

• 3e6edb6a...f2640c5e - 3 commits from branch iris:master
• b55c6735 - simplify telescope-based notations

Compare with previous version

marked this merge request as ready

removed S-draft label

enabled an automatic merge when the pipeline for b55c6735 succeeds

Strange, why does this fail on Coq 8.12...

It works in 8.13. I am tempted to just drop 8.12... 8.14 is released so this would be in accordance with our policy of supporting the latest 2 Coq versions.

mentioned in merge request !763 (merged)

changed the description

added 26 commits

• b55c6735...6dfda15b - 25 commits from branch iris:master
• ea0b55fa - simplify telescope-based notations

Compare with previous version

enabled an automatic merge when the pipeline for ea0b55fa succeeds

merged

mentioned in commit ec0acc9c