Merge branch 'v8.5'

4 files changed, 37 insertions, 10 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 926b38794..b6df8f454 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -182,14 +182,17 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+  let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
-      (List.map (fun (id, _,_) -> Id.to_string id)
-        (keep_hyps env (Id.Set.union s1 s2))) in
-  Aux_file.record_in_aux "context_used" v
+      (CList.map_filter (fun (id, _,_) ->
+          if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
 
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -204,6 +207,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
@@ -221,19 +228,21 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            !suggest_proof_using kn env vars ids_typ context_ids;
+            let expr =
+              !suggest_proof_using (Constant.to_string kn)
+                env vars ids_typ context_ids in
             if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars;
+              record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
-          record_aux env Id.Set.empty Id.Set.empty;
+          record_aux env Id.Set.empty Id.Set.empty "";
         [], 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 ->
@@ -303,6 +312,20 @@ let translate_local_def env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
     infer_declaration env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
+  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+    match def with
+    | Undef _ -> ()
+    | Def _ -> ()
+    | OpaqueDef lc ->
+       let context_ids = List.map pi1 (named_context env) in
+       let ids_typ = global_vars_set env typ in
+       let ids_def = global_vars_set env
+         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let expr =
+         !suggest_proof_using (Id.to_string id)
+           env ids_def ids_typ context_ids in
+       record_aux env ids_typ ids_def expr
+  end;
   def, typ, univs
 
 (* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea1..8d92bcc68 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -44,4 +44,4 @@ val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
-  (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
+  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7e6d4de23..8201980e3 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1020,6 +1020,9 @@ struct
   let empty = (LSet.empty, Constraint.empty)
   let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
 
+  let equal (univs, cst as x) (univs', cst' as y) =
+    x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
+									
   let of_set s = (s, Constraint.empty)
   let singleton l = of_set (LSet.singleton l)
   let of_instance i = of_set (Instance.levels i)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index dbbc83262..ae7400337 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -325,6 +325,7 @@ sig
   val of_instance : Instance.t -> t
   val of_set : universe_set -> t
 
+  val equal : t -> t -> bool
   val union : t -> t -> t
 
   val append : t -> t -> t