| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | CheckerMaker.v | 4858 | logplain |
| -rw-r--r-- | Env.v | 4832 | logplain |
| -rw-r--r-- | EnvRing.v | 43817 | logplain |
| -rw-r--r-- | LICENSE.sos | 1583 | logplain |
| -rw-r--r-- | MExtraction.v | 2021 | logplain |
| -rw-r--r-- | OrderedRing.v | 14123 | logplain |
| -rw-r--r-- | Psatz.v | 3090 | logplain |
| -rw-r--r-- | QMicromega.v | 6385 | logplain |
| -rw-r--r-- | RMicromega.v | 5408 | logplain |
| -rw-r--r-- | Refl.v | 3519 | logplain |
| -rw-r--r-- | RingMicromega.v | 27386 | logplain |
| -rw-r--r-- | Tauto.v | 8985 | logplain |
| -rw-r--r-- | VarMap.v | 6710 | logplain |
| -rw-r--r-- | ZCoeff.v | 5258 | logplain |
| -rw-r--r-- | ZMicromega.v | 32775 | logplain |
| -rw-r--r-- | certificate.ml | 25518 | logplain |
| -rw-r--r-- | coq_micromega.ml | 46764 | logplain |
| -rw-r--r-- | csdpcert.ml | 6260 | logplain |
| -rw-r--r-- | g_micromega.ml4 | 2106 | logplain |
| -rw-r--r-- | mfourier.ml | 31747 | logplain |
| -rw-r--r-- | micromega.ml | 51980 | logplain |
| -rw-r--r-- | micromega.mli | 10102 | logplain |
| -rw-r--r-- | micromega_plugin.mllib | 102 | logplain |
| -rw-r--r-- | mutils.ml | 9259 | logplain |
| -rw-r--r-- | persistent_cache.ml | 4614 | logplain |
| -rw-r--r-- | sos.ml | 71017 | logplain |
| -rw-r--r-- | sos.mli | 1781 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |