Skip to content
GitLab

Make `solve_inG` faster.

Merged Robbert Krebbers requested to merge robbert/issue_347 into master
  1. First simpl away all the functors
  2. Don't use done, which calls split
  3. Define non-unital camera functors in such a way that the non-unital camera is used.

(3) involves partially rolling back !498 (merged), but I have done that in a way that the proofs don't need to be repeated.

Helps with #347.

Edited by Ralf Jung