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.

1 files changed, 5 insertions, 1 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 926b38794..8eb920fb7 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -204,6 +204,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
+  let sort evn l =
+    List.filter (fun (id,_,_) ->
+      List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+    (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map pi1 (named_context env) in
@@ -233,7 +237,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
-        declared,
+        sort env declared,
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->