index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
setoid_ring
Mode
Name
Size
-rw-r--r--
Algebra_syntax.v
1599
log
plain
-rw-r--r--
ArithRing.v
2283
log
plain
-rw-r--r--
BinList.v
2358
log
plain
-rw-r--r--
Cring.v
9132
log
plain
-rw-r--r--
Field.v
731
log
plain
-rw-r--r--
Field_tac.v
19722
log
plain
-rw-r--r--
Field_theory.v
54489
log
plain
-rw-r--r--
InitialRing.v
26874
log
plain
-rw-r--r--
Integral_domain.v
1980
log
plain
-rw-r--r--
NArithRing.v
919
log
plain
-rw-r--r--
Ncring.v
9630
log
plain
-rw-r--r--
Ncring_initial.v
6355
log
plain
-rw-r--r--
Ncring_polynom.v
17144
log
plain
-rw-r--r--
Ncring_tac.v
9589
log
plain
-rw-r--r--
RealField.v
4175
log
plain
-rw-r--r--
Ring.v
1604
log
plain
-rw-r--r--
Ring_base.v
967
log
plain
-rw-r--r--
Ring_polynom.v
43391
log
plain
-rw-r--r--
Ring_tac.v
15724
log
plain
-rw-r--r--
Ring_theory.v
19173
log
plain
-rw-r--r--
Rings_Q.v
1455
log
plain
-rw-r--r--
Rings_R.v
1595
log
plain
-rw-r--r--
Rings_Z.v
1004
log
plain
-rw-r--r--
ZArithRing.v
1692
log
plain
-rw-r--r--
g_newring.ml4
5666
log
plain
-rw-r--r--
newring.ml
39987
log
plain
-rw-r--r--
newring.mli
1404
log
plain
-rw-r--r--
newring_ast.ml
2197
log
plain
-rw-r--r--
newring_ast.mli
2197
log
plain
-rw-r--r--
newring_plugin.mlpack
30
log
plain
