<commit_before>open Pp
open Util
open Names
open Cic
open Term
open Reduction
open Typeops
open Indtypes
open Modops
open Subtyping
open Declarations
open Environ

(** {6 Checking constants } *)

let refresh_arity ar =
  let ctxt, hd = decompose_prod_assum ar in
  match hd with
      Sort (Type u) when not (Univ.is_univ_variable u) ->
      let ul = Univ.Level.make DirPath.empty 1 in
      let u' = Univ.Universe.make ul in
      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
        mkArity (ctxt,Prop Null), ctx
    | _ -> ar, Univ.ContextSet.empty

let check_constant_declaration env kn cb =
  Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
  (** [env'] contains De Bruijn universe variables *)
  let env' =
    match cb.const_universes with
    | Monomorphic_const ctx -> push_context ~strict:true ctx env
    | Polymorphic_const auctx ->
      let ctx = Univ.AUContext.repr auctx in
      push_context ~strict:false ctx env
  in
  let envty, ty = 
    let ty = cb.const_type in
    let ty', cu = refresh_arity ty in<commit_msg>Fix -silent flag of coqchk after ff918e4.<commit_after>open Pp
open Util
open Names
open Cic
open Term
open Reduction
open Typeops
open Indtypes
open Modops
open Subtyping
open Declarations
open Environ

(** {6 Checking constants } *)

let refresh_arity ar =
  let ctxt, hd = decompose_prod_assum ar in
  match hd with
      Sort (Type u) when not (Univ.is_univ_variable u) ->
      let ul = Univ.Level.make DirPath.empty 1 in
      let u' = Univ.Universe.make ul in
      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
        mkArity (ctxt,Prop Null), ctx
    | _ -> ar, Univ.ContextSet.empty

let check_constant_declaration env kn cb =
  Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
  (** [env'] contains De Bruijn universe variables *)
  let env' =
    match cb.const_universes with
    | Monomorphic_const ctx -> push_context ~strict:true ctx env
    | Polymorphic_const auctx ->
      let ctx = Univ.AUContext.repr auctx in
      push_context ~strict:false ctx env
  in
  let envty, ty = 
    let ty = cb.const_type in
    let ty', cu = refresh_arity ty in
{'fraction_non_alphanumeric': 0.07973856209150326, 'fraction_numerical': 0.003485838779956427, 'mean_word_length': 3.136936936936937, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5735204', 'n_tokens_mistral': 791, 'n_tokens_neox': 762, 'n_words': 266}