Indfun_common (rocq-runtime.Funind_plugin.Indfun

val mk_rel_id : Names.Id.t -> Names.Id.t

val mk_correct_id : Names.Id.t -> Names.Id.t

val mk_complete_id : Names.Id.t -> Names.Id.t

val mk_equation_id : Names.Id.t -> Names.Id.t

val fresh_id : Names.Id.t list -> string -> Names.Id.t

val fresh_name : Names.Id.t list -> string -> Names.Name.t

val get_name : 
  Names.Id.t list ->
  ?default:string ->
  Names.Name.t ->
  Names.Name.t

val array_get_start : 'a array -> 'a array

val locate_ind : Libnames.qualid -> Names.inductive

val locate_constant : Libnames.qualid -> Names.Constant.t

val locate_with_msg : Pp.t -> (Libnames.qualid -> 'a) -> Libnames.qualid -> 'a

val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list

val list_union_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list

val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list

val chop_rlambda_n : 
  int ->
  Glob_term.glob_constr ->
  (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list
  * Glob_term.glob_constr

val chop_rprod_n : 
  int ->
  Glob_term.glob_constr ->
  (Names.Name.t * Glob_term.glob_constr) list * Glob_term.glob_constr

val eq : unit -> EConstr.constr

val refl_equal : unit -> EConstr.constr

val jmeq : unit -> EConstr.constr

val jmeq_refl : unit -> EConstr.constr

val make_eq : unit -> EConstr.constr

val without_implicit_declarations : (unit -> unit) -> unit -> unit

Run the function with auto implicits off and dumglob paused

val full_printing_flags : unit -> PrintingFlags.t

val extern_env_full_printing : unit -> Constrextern.extern_env

type function_info = {

function_constant : Names.Constant.t;
graph_ind : Names.inductive;
equation_lemma : Names.Constant.t option;
correctness_lemma : Names.Constant.t option;
completeness_lemma : Names.Constant.t option;
rect_lemma : Names.Constant.t option;
rec_lemma : Names.Constant.t option;
prop_lemma : Names.Constant.t option;
sprop_lemma : Names.Constant.t option;
is_general : bool;

}

val find_Function_infos : Names.Constant.t -> function_info option

val find_Function_of_graph : Names.inductive -> function_info option

val add_Function : bool -> Names.Constant.t -> unit

val update_Function : function_info -> unit

val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t

debugging

val pr_table : Environ.env -> Evd.evar_map -> Pp.t

val observe_tac : 
  header:Pp.t ->
  (Environ.env -> Evd.evar_map -> Pp.t) ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val observe : CDebug.t

val do_observe : unit -> bool

val do_rewrite_dependent : unit -> bool

exception Building_graph of exn

exception Defining_principle of exn

exception ToShow of exn

val is_strict_tcc : unit -> bool

val h_intros : Names.Id.t list -> unit Proofview.tactic

val h_id : Names.Id.t

val hrec_id : Names.Id.t

val acc_inv_id : EConstr.constr Util.delayed

val ltof_ref : Names.GlobRef.t Util.delayed

val well_founded_ltof : EConstr.constr Util.delayed

val acc_rel : EConstr.constr Util.delayed

val well_founded : EConstr.constr Util.delayed

val evaluable_of_global_reference : Names.GlobRef.t -> Evaluable.t

val list_rewrite : 
  bool ->
  (EConstr.constr * bool) list ->
  unit Proofview.tactic

val decompose_lambda_n : 
  Evd.evar_map ->
  int ->
  EConstr.t ->
  (Names.Name.t EConstr.binder_annot * EConstr.t) list * EConstr.t

val compose_lam : 
  (Names.Name.t EConstr.binder_annot * EConstr.t) list ->
  EConstr.t ->
  EConstr.t

val compose_prod : 
  (Names.Name.t EConstr.binder_annot * EConstr.t) list ->
  EConstr.t ->
  EConstr.t

type tcc_lemma_value =

| Undefined
| Value of Constr.t
| Not_needed

val funind_purify : ('a -> 'b) -> 'a -> 'b