G_indfun (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.funind_plugin.Funind_plugin.G

Source

val wit_fun_ind_using : 
  (Constrexpr.constr_expr Tactypes.with_bindings option,
    Genintern.glob_constr_and_expr Tactypes.with_bindings option,
    EConstr.constr Tactypes.with_bindings Tactypes.delayed_open option)
    Genarg.genarg_type

Source

val fun_ind_using : 
  Constrexpr.constr_expr Tactypes.with_bindings option Procq.Entry.t

Source

val wit_with_names : 
  (Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option,
    Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option,
    Tactypes.intro_pattern option)
    Genarg.genarg_type

Source

val with_names : 
  Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option
    Procq.Entry.t

Source

val wit_function_fix_definition : 
  Vernacexpr.fixpoint_expr Loc.located Genarg.vernac_genarg_type

Source

val function_fix_definition : 
  Vernacexpr.fixpoint_expr Loc.located Procq.Entry.t

Source

val wit_fun_scheme_arg : 
  (Names.Id.t * Libnames.qualid * Sorts.family) Genarg.vernac_genarg_type

Source

val fun_scheme_arg : 
  (Names.Id.t * Libnames.qualid * Sorts.family) Procq.Entry.t