Module Ring_plugin.Ring_ast

type 'constr coeff_spec =
| Computational of 'constr
| Abstract
| Morphism of 'constr
type cst_tac_spec =
| CstTac of Ltac_plugin.Tacexpr.raw_tactic_expr
| Closed of Libnames.qualid list
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 'constr field_mod =
| Ring_mod of 'constr ring_mod
| Inject 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;
}