package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.1.tar.gz

sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/ring_plugin/Ring_plugin/Ring_ast/index.html

Module `Ring_plugin.Ring_ast`Source

Sourcetype 'constr coeff_spec =

| Computational of 'constr
| Abstract
| Morphism of 'constr

Sourcetype cst_tac_spec =

| CstTac of Ltac_plugin.Tacexpr.raw_tactic_expr
| Closed of Libnames.qualid list

Sourcetype '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

Sourcetype 'constr field_mod =

| Ring_mod of 'constr ring_mod
| Inject of Constrexpr.constr_expr

Sourcetype 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;

}

Sourcetype 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;

}