term_typing: strengthen discharging code

Given the way Lib.extract_hyps is coded if the const_hyps field
of a constant declaration contains a named_context that does not
have the same order of the one in Environment.env, discharging is
broken (as in some section variables are not discharged).
If const_hyps is computed by the kernel, then the order is correct by
construction.  If such list is provided by the user, the order is not
granted.

We now systematically sort the list of user provided section hyps.

The code of Proof using is building the named_context in the right
order, but the API was not enforcing/checking it.  Now it does.

0 files changed, 0 insertions, 0 deletions