diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 33 |
1 files changed, 10 insertions, 23 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 10221e18e9..b3c3dcbf45 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -151,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; cook_inline = false; - cook_context = c.opaque_entry_secctx; + cook_context = Some c.opaque_entry_secctx; } (** Similar case for polymorphic entries. *) @@ -188,7 +188,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; cook_inline = false; - cook_context = c.opaque_entry_secctx; + cook_context = Some c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) @@ -237,17 +237,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } -let record_aux env s_ty s_bo = - let in_ty = keep_hyps env s_ty in - let v = - String.concat " " - (CList.map_filter (fun decl -> - let id = NamedDecl.get_id decl in - if List.exists (NamedDecl.get_id %> Id.equal 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 - let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in @@ -279,24 +268,22 @@ let build_constant_declaration env result = let context_ids = List.map NamedDecl.get_id (named_context env) in let def = result.cook_body in match result.cook_context with - | None when not (List.is_empty context_ids) -> + | None -> + if List.is_empty context_ids then + (* Empty section context: no need to check *) + [], def + else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) let ids_typ = global_vars_set env typ in let ids_def = match def with | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) - | OpaqueDef lc -> - let (lc, _) = Future.force lc in - let vars = global_vars_set env lc in - if !Flags.record_aux_file then record_aux env ids_typ vars; - vars + | OpaqueDef _ -> + (* Opaque definitions always come with their section variables *) + assert false in keep_hyps env (Id.Set.union ids_typ ids_def), def - | None -> - if !Flags.record_aux_file then - 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 *) sort declared, |