| 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 | 26504 | logplain |
| -rw-r--r-- | Tauto.v | 8929 | logplain |
| -rw-r--r-- | VarMap.v | 6710 | logplain |
| -rw-r--r-- | ZCoeff.v | 5258 | logplain |
| -rw-r--r-- | ZMicromega.v | 32214 | logplain |
| -rw-r--r-- | certificate.ml | 25518 | logplain |
| -rw-r--r-- | coq_micromega.ml | 46647 | logplain |
| -rw-r--r-- | csdpcert.ml | 6086 | 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 | 8864 | logplain |
| -rw-r--r-- | persistent_cache.ml | 4893 | logplain |
| -rw-r--r-- | sos.ml | 71021 | logplain |
| -rw-r--r-- | sos.mli | 1781 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |