Move the responsibility of type-checking to the caller for tactic-in-terms.

Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.

This should be 1:1 equivalent to the previous code, we are just moving code
around.

0 files changed, 0 insertions, 0 deletions