From 0f706b470c83a957b600496c2bca652c2cfe65e3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 7 Oct 2015 13:36:03 +0200
Subject: 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.
---
 kernel/term_typing.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 926b387942..8eb920fb78 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 ->
-- 
cgit v1.2.3