Annotate telescope notations to support literal telescope arguments.

!368 (merged) had the unfortunate consequence that literal telescope arguments would not typecheck any more. This MR fixes this by adding copious (but nonetheless minimal) amounts of casts and annotations to make the [tele_arg ..] notation work again. I added tests for both new and old unification.

I am currently running a full test with these changes on all BedRock proofs which should tell us a bit about the compatibility. I expect no problems here.

Something that is not reflected in the MR but is still interesting is that old unification, i.e. apply and friends, work even without the cast in the TargS notation. New unification, i.e. refine, does not. There might be a Coq bug to report here but I don't have time to dig into that right now.

Something that is not reflected in the MR but is still interesting is that old unification, i.e. apply and friends, work even without the cast in the TargS notation. New unification, i.e. refine, does not. There might be a Coq bug to report here but I don't have time to dig into that right now.

Could you add that as a testcase, with comments explaining the situation?

added 1 commit

• d1bec90c - Document reasons for using both `exact` and `refine`.

Compare with previous version

resolved all threads

merged

mentioned in commit 1aceb4c6