package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `ComInductive.Internal`Source

val error_differing_params : 
  kind:string ->
  (Names.lident * Vernacexpr.inductive_params_expr) ->
  (Names.lident * Vernacexpr.inductive_params_expr) ->
  'a