| 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 | 3703 | logplain |
| -rw-r--r-- | QMicromega.v | 7571 | logplain |
| -rw-r--r-- | RMicromega.v | 5210 | 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 | 21450 | logplain |
| -rw-r--r-- | certificate.ml | 23152 | logplain |
| -rw-r--r-- | coq_micromega.ml | 40456 | logplain |
| -rw-r--r-- | csdpcert.ml | 6415 | logplain |
| -rw-r--r-- | g_micromega.ml4 | 2104 | logplain |
| -rw-r--r-- | mfourier.ml | 18349 | logplain |
| -rw-r--r-- | micromega.ml | 45757 | logplain |
| -rw-r--r-- | micromega.mli | 8809 | logplain |
| -rw-r--r-- | mutils.ml | 6874 | logplain |
| -rw-r--r-- | sos.ml | 73016 | logplain |
| -rw-r--r-- | sos.mli | 1781 | logplain |
| -rw-r--r-- | vector.ml | 15256 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |