index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
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
9160
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
55513
log
plain
-rw-r--r--
InitialRing.v
26884
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
6378
log
plain
-rw-r--r--
Ncring_polynom.v
17167
log
plain
-rw-r--r--
Ncring_tac.v
9751
log
plain
-rw-r--r--
RealField.v
4318
log
plain
-rw-r--r--
Ring.v
1604
log
plain
-rw-r--r--
Ring_base.v
945
log
plain
-rw-r--r--
Ring_polynom.v
43736
log
plain
-rw-r--r--
Ring_tac.v
15702
log
plain
-rw-r--r--
Ring_theory.v
19163
log
plain
-rw-r--r--
Rings_Q.v
1464
log
plain
-rw-r--r--
Rings_R.v
1604
log
plain
-rw-r--r--
Rings_Z.v
1017
log
plain
-rw-r--r--
ZArithRing.v
1692
log
plain
-rw-r--r--
g_newring.mlg
4952
log
plain
-rw-r--r--
newring.ml
37822
log
plain
-rw-r--r--
newring.mli
1293
log
plain
-rw-r--r--
newring_ast.ml
2258
log
plain
-rw-r--r--
newring_ast.mli
2258
log
plain
-rw-r--r--
newring_plugin.mlpack
30
log
plain
-rw-r--r--
plugin_base.dune
141
log
plain
