aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-07 13:36:03 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-08 09:51:13 +0200
commit0f706b470c83a957b600496c2bca652c2cfe65e3 (patch)
tree2f012f1f7c6be8bae34be5e40615b5c0873b4ae5 /kernel/term_typing.mli
parent27bad55f6f87af2ae3ad7921d71c02e333a853bb (diff)
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.
Diffstat (limited to 'kernel/term_typing.mli')
0 files changed, 0 insertions, 0 deletions