package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Funind_plugin.G_indfun`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.lident * Libnames.qualid * UnivGen.QualityOrSet.t)
    Genarg.vernac_genarg_type

Source

val fun_scheme_arg : 
  (Names.lident * Libnames.qualid * UnivGen.QualityOrSet.t) Procq.Entry.t

package rocq-runtime

Module Funind_plugin.G_indfunSource

Module `Funind_plugin.G_indfun`Source