<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by <NAME> from contents related to lemma proofs in
   file command.ml, Aug 2009 *)

open CErrors
open Util
open Flags
open Pp
open Names
open Term
open Declarations
open Declareops
open Entries
open Environ
open Nameops
open Globnames
open Decls
open Decl_kinds
open Declare
open Pretyping
open Termops
open Namegen
open Reductionops
open Constrexpr
open Constrintern
open Impargs
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
let mk_hook hook = hook
let call_hook fix_exn hook l c =
  try hook l c
  with e when CErrors.noncritical e ->
    let e = CErrors.push e in
    iraise (fix_exn e)

(* Support for mutually proved theorems *)

let retrieve_first_recthm = function
  | VarRef id ->
      (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
  | ConstRef cst ->
      let cb = Global.lookup_constant cst in
      (Global.body_of_constant_body cb, is_opaque cb)
  | _ -> assert false<commit_msg>Fix two new unused opens.<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by <NAME> from contents related to lemma proofs in
   file command.ml, Aug 2009 *)

open CErrors
open Util
open Flags
open Pp
open Names
open Term
open Declarations
open Declareops
open Entries
open Environ
open Nameops
open Globnames
open Decls
open Decl_kinds
open Declare
open Pretyping
open Termops
open Namegen
open Reductionops
open Constrintern
open Impargs

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
let mk_hook hook = hook
let call_hook fix_exn hook l c =
  try hook l c
  with e when CErrors.noncritical e ->
    let e = CErrors.push e in
    iraise (fix_exn e)

(* Support for mutually proved theorems *)

let retrieve_first_recthm = function
  | VarRef id ->
      (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
  | ConstRef cst ->
      let cb = Global.lookup_constant cst in
      (Global.body_of_constant_body cb, is_opaque cb)
  | _ -> assert false
{'fraction_non_alphanumeric': 0.19414147709566842, 'fraction_numerical': 0.008725459644749143, 'mean_word_length': 3.692982456140351, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 17, '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': '5584541', 'n_tokens_mistral': 946, 'n_tokens_neox': 884, 'n_words': 321}