Commit 2023-11-22 06:12 af56a1ad

fix: elaborate linarith arguments without errToSorry (#8561) This means that linarith will fail before executing its algorithm if there is an elaboration error in one of its supplied terms, rather than going ahead and silently failing. Also, checks for new metavariables in the elaborated terms, which can't be used since linarith is a finishing tactic. Lastly, copies these (and pre-existing) fixes to nlinarith.