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
924
log
plain
-rw-r--r--
ArithRing.v
2133
log
plain
-rw-r--r--
BinList.v
2208
log
plain
-rw-r--r--
Cring.v
8982
log
plain
-rw-r--r--
Field.v
581
log
plain
-rw-r--r--
Field_tac.v
19572
log
plain
-rw-r--r--
Field_theory.v
54339
log
plain
-rw-r--r--
InitialRing.v
26724
log
plain
-rw-r--r--
Integral_domain.v
1304
log
plain
-rw-r--r--
NArithRing.v
769
log
plain
-rw-r--r--
Ncring.v
9480
log
plain
-rw-r--r--
Ncring_initial.v
6205
log
plain
-rw-r--r--
Ncring_polynom.v
16994
log
plain
-rw-r--r--
Ncring_tac.v
9439
log
plain
-rw-r--r--
RealField.v
3499
log
plain
-rw-r--r--
Ring.v
1454
log
plain
-rw-r--r--
Ring_base.v
817
log
plain
-rw-r--r--
Ring_polynom.v
43241
log
plain
-rw-r--r--
Ring_tac.v
15048
log
plain
-rw-r--r--
Ring_theory.v
19019
log
plain
-rw-r--r--
Rings_Q.v
779
log
plain
-rw-r--r--
Rings_R.v
919
log
plain
-rw-r--r--
Rings_Z.v
328
log
plain
-rw-r--r--
ZArithRing.v
1542
log
plain
-rw-r--r--
g_newring.ml4
5565
log
plain
-rw-r--r--
newring.ml
39770
log
plain
-rw-r--r--
newring.mli
1276
log
plain
-rw-r--r--
newring_ast.mli
2032
log
plain
-rw-r--r--
newring_plugin.mlpack
18
log
plain