index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
micromega
Mode
Name
Size
-rw-r--r--
DeclConstant.v
2823
log
plain
-rw-r--r--
Env.v
3249
log
plain
-rw-r--r--
EnvRing.v
31591
log
plain
-rw-r--r--
Fourier.v
129
log
plain
-rw-r--r--
Fourier_util.v
699
log
plain
-rw-r--r--
LICENSE.sos
1583
log
plain
-rw-r--r--
Lia.v
1733
log
plain
-rw-r--r--
Lqa.v
2183
log
plain
-rw-r--r--
Lra.v
2216
log
plain
-rw-r--r--
MExtraction.v
2844
log
plain
-rw-r--r--
OrderedRing.v
14270
log
plain
-rw-r--r--
Psatz.v
2208
log
plain
-rw-r--r--
QMicromega.v
7309
log
plain
-rw-r--r--
RMicromega.v
12642
log
plain
-rw-r--r--
Refl.v
4254
log
plain
-rw-r--r--
RingMicromega.v
33998
log
plain
-rw-r--r--
Tauto.v
39491
log
plain
-rw-r--r--
VarMap.v
2720
log
plain
-rw-r--r--
ZCoeff.v
5561
log
plain
-rw-r--r--
ZMicromega.v
48715
log
plain
-rw-r--r--
Zify.v
3169
log
plain
-rw-r--r--
ZifyBool.v
7926
log
plain
-rw-r--r--
ZifyClasses.v
8725
log
plain
-rw-r--r--
ZifyComparison.v
2535
log
plain
-rw-r--r--
ZifyInst.v
14860
log
plain
-rw-r--r--
Ztac.v
3607
log
plain
-rw-r--r--
certificate.ml
34640
log
plain
-rw-r--r--
certificate.mli
2362
log
plain
-rw-r--r--
coq_micromega.ml
82437
log
plain
-rw-r--r--
coq_micromega.mli
1643
log
plain
-rw-r--r--
csdpcert.ml
6709
log
plain
-rw-r--r--
csdpcert.mli
675
log
plain
-rw-r--r--
g_micromega.mlg
3277
log
plain
-rw-r--r--
g_micromega.mli
675
log
plain
-rw-r--r--
g_zify.mlg
2141
log
plain
-rw-r--r--
itv.ml
2514
log
plain
-rw-r--r--
itv.mli
983
log
plain
-rw-r--r--
mfourier.ml
26561
log
plain
-rw-r--r--
mfourier.mli
1137
log
plain
-rw-r--r--
micromega.ml
64049
log
plain
-rw-r--r--
micromega.mli
17259
log
plain
-rw-r--r--
micromega_plugin.mlpack
119
log
plain
-rw-r--r--
mutils.ml
12646
log
plain
-rw-r--r--
mutils.mli
4013
log
plain
-rw-r--r--
persistent_cache.ml
5389
log
plain
-rw-r--r--
persistent_cache.mli
1713
log
plain
-rw-r--r--
plugin_base.dune
560
log
plain
-rw-r--r--
polynomial.ml
33655
log
plain
-rw-r--r--
polynomial.mli
11379
log
plain
-rw-r--r--
simplex.ml
24533
log
plain
-rw-r--r--
simplex.mli
1229
log
plain
-rw-r--r--
sos.ml
45621
log
plain
-rw-r--r--
sos.mli
1306
log
plain
-rw-r--r--
sos_lib.ml
19236
log
plain
-rw-r--r--
sos_lib.mli
3072
log
plain
-rw-r--r--
sos_types.ml
2763
log
plain
-rw-r--r--
sos_types.mli
1405
log
plain
-rw-r--r--
vect.ml
8886
log
plain
-rw-r--r--
vect.mli
6510
log
plain
-rw-r--r--
zify.ml
33338
log
plain
-rw-r--r--
zify.mli
1217
log
plain
-rw-r--r--
zify_plugin.mlpack
12
log
plain