package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Funind_plugin.Indfun`Source

val functional_induction : 
  bool ->
  EConstr.constr ->
  (EConstr.constr * EConstr.constr Tactypes.bindings) option ->
  Tactypes.or_and_intro_pattern option ->
  unit Proofview.tactic