Funind_plugin.Glob_term_to_relation
val build_inductive :
Evd.evar_map ->
Constr.pconstant list ->
(Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list
list ->
Constrexpr.constr_expr list ->
Glob_term.glob_constr list ->
unit