<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Util
open Names
open Univ
open Term
open Reduction
open Sign
open Declarations
open Inductive
open Environ
open Entries
open Type_errors
open Cemitcodes
open Cbytegen
open Indtypes
open Typeops

let constrain_type env j cst1 = function
  | None -> j.uj_type, cst1
  | Some t -> 
      let (tj,cst2) = infer_type env t in
      let cst3 =
	try vm_conv_leq env j.uj_type tj.utj_val
	with NotConvertible -> error_actual_type env j tj.utj_val in
      let typ = 
        if t = tj.utj_val then t else
          (error "Kernel built a type different from its input\n";
           flush stdout; tj.utj_val) in
      typ, Constraint.union (Constraint.union cst1 cst2) cst3


let translate_local_def env (b,topt) =
  let (j,cst) = infer env b in<commit_msg>Nettoyage suite nouvel avertissement Z de ocaml 3.09<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Util
open Names
open Univ
open Term
open Reduction
open Sign
open Declarations
open Inductive
open Environ
open Entries
open Type_errors
open Cemitcodes
open Cbytegen
open Indtypes
open Typeops

let constrain_type env j cst1 = function
  | None -> j.uj_type, cst1
  | Some t -> 
      let (tj,cst2) = infer_type env t in
      let cst3 =
	try vm_conv_leq env j.uj_type tj.utj_val
	with NotConvertible -> error_actual_type env j tj.utj_val in
      assert (t = tj.utj_val);
      t, Constraint.union (Constraint.union cst1 cst2) cst3


let translate_local_def env (b,topt) =
  let (j,cst) = infer env b in
{'fraction_non_alphanumeric': 0.23373015873015873, 'fraction_numerical': 0.008333333333333333, 'mean_word_length': 3.438380281690141, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4972089', 'n_tokens_mistral': 780, 'n_tokens_neox': 739, 'n_words': 252}