Generalize frac to dfrac in auth and view camera

view and all of its clients takes a dfrac instead of a frac.

Closes #395 (closed).

Todo

• Add CHANGELOG entry.

changed title from Generalize frac to dfrac in view camera to Generalize frac to dfrac in auth and view camera

added 15 commits

• 8a3c6ae9...d41f8ad5 - 13 commits from branch iris:master
• 3dd919c1 - Make view auth take dfrac
• 3b602f22 - Name lemmas about dfrac accordingly

Compare with previous version

changed the description

I am not sure what's the current status of this MR is, so let me try to summarize:

• We need to figure out if we want to keep auth_auth_frac_op or not. I think it makes sense to have it, otherwise when using concrete fractions, users end up with goals that involve ●{DfracOwn q1 ⋅ DfracOwn q2} ..., which does not seem too readable. Similarly, for auth_auth_frac_op_valid(N?) we might want to do the same, otherwise we essentially end up undoing !558 (merged).
• We decide to generalize auth and view, and not the other derived constructions. Those will be done in a future MR. An exception is gset_bij because that one has already been done.

added 1 commit

• 1e80ec71 - Name lemmas about dfrac accordingly

Compare with previous version

Modulo some small points, I think this MR is ready.

Can you try to have a sweep through the files you ported and replace variables q by dq where applicable? I think these inconsistencies can be automatically detected by adding:

Implicit Types q : frac.
Implicit Types dq : dfrac.

To the beginning of the Sections.

added 78 commits

• 1e80ec71...5bb93f57 - 76 commits from branch iris:master
• 1942901f - Make view auth take dfrac
• 7ede62ae - Name lemmas about dfrac accordingly

Compare with previous version

added 1 commit

• 1208395a - Name lemmas about dfrac accordingly

Compare with previous version

added 1 commit

• dd8818fb - Add changelog entry for auth and view changes

Compare with previous version

marked the checklist item Add CHANGELOG entry. as completed

I've addressed the latest comments and added a CHANGELOG entry with a sed script that seems to work well to handle all the renaming.

Note that I've added a new section to the CHANGELOG for changes to master. If other/future MRs do the same they will conflict.

resolved all threads