Ring_plugin.Ring_ast
type 'constr ring_mod =
| Ring_kind of 'constr coeff_spec |
| Const_tac of cst_tac_spec |
| Pre_tac of Ltac_plugin.Tacexpr.raw_tactic_expr |
| Post_tac of Ltac_plugin.Tacexpr.raw_tactic_expr |
| Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr |
| Pow_spec of cst_tac_spec * Constrexpr.constr_expr |
| Sign_spec of Constrexpr.constr_expr |
| Div_spec of Constrexpr.constr_expr |
type ring_info = {
ring_name : Names.Id.t; |
ring_carrier : Constr.types; |
ring_req : Constr.constr; |
ring_setoid : Constr.constr; |
ring_ext : Constr.constr; |
ring_morph : Constr.constr; |
ring_th : Constr.constr; |
ring_cst_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
ring_pow_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
ring_lemma1 : Constr.constr; |
ring_lemma2 : Constr.constr; |
ring_pre_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
ring_post_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
}
type field_info = {
field_name : Names.Id.t; |
field_carrier : Constr.types; |
field_req : Constr.constr; |
field_cst_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
field_pow_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
field_ok : Constr.constr; |
field_simpl_eq_ok : Constr.constr; |
field_simpl_ok : Constr.constr; |
field_simpl_eq_in_ok : Constr.constr; |
field_cond : Constr.constr; |
field_pre_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
field_post_tac : Ltac_plugin.Tacexpr.glob_tactic_expr; |
}