Parameter Make.A

type a

Type and name of the analysis result

val name : string
val default : string -> a option

Default value. This is called for generic arguments not registered via a plugin. If None, Rocq will emit an anomaly when a non-registered generic argument is found. The argument is the name of the non-handled generic argument.

val fold_list : a list -> a

Combine results of analysis, for standard genarg types

val fold_option : a option -> a
val fold_pair : (a * a) -> a