| 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 | 1266 | 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 | 26616 | 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 | 24695 | logplain |
| -rw-r--r-- | coq_micromega.ml | 45294 | logplain |
| -rw-r--r-- | csdpcert.ml | 6415 | logplain |
| -rw-r--r-- | g_micromega.ml4 | 2104 | logplain |
| -rw-r--r-- | mfourier.ml | 31749 | logplain |
| -rw-r--r-- | micromega.ml | 45757 | logplain |
| -rw-r--r-- | micromega.mli | 8809 | logplain |
| -rw-r--r-- | micromega_plugin.mllib | 85 | logplain |
| -rw-r--r-- | mutils.ml | 7652 | logplain |
| -rw-r--r-- | sos.ml | 73016 | logplain |
| -rw-r--r-- | sos.mli | 1781 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |