Module Newring_plugin.Newring_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;
}