| 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 | 1898 | logplain |
| -rw-r--r-- | OrderedRing.v | 14123 | logplain |
| -rw-r--r-- | Psatz.v | 3034 | logplain |
| -rw-r--r-- | QMicromega.v | 6435 | logplain |
| -rw-r--r-- | RMicromega.v | 5241 | logplain |
| -rw-r--r-- | Refl.v | 3519 | logplain |
| -rw-r--r-- | RingMicromega.v | 26668 | logplain |
| -rw-r--r-- | Tauto.v | 8931 | logplain |
| -rw-r--r-- | VarMap.v | 6710 | logplain |
| -rw-r--r-- | ZCoeff.v | 5258 | logplain |
| -rw-r--r-- | ZMicromega.v | 21296 | logplain |
| -rw-r--r-- | certificate.ml | 24587 | logplain |
| -rw-r--r-- | coq_micromega.ml | 44503 | logplain |
| -rw-r--r-- | csdpcert.ml | 6380 | logplain |
| -rw-r--r-- | g_micromega.ml4 | 2104 | logplain |
| -rw-r--r-- | mfourier.ml | 31749 | logplain |
| -rw-r--r-- | micromega.ml | 43075 | logplain |
| -rw-r--r-- | micromega.mli | 8542 | logplain |
| -rw-r--r-- | micromega_plugin.mllib | 85 | logplain |
| -rw-r--r-- | mutils.ml | 7402 | logplain |
| -rw-r--r-- | sos.ml | 73016 | logplain |
| -rw-r--r-- | sos.mli | 1781 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |