| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | DeclConstant.v | 2885 | logplain |
| -rw-r--r-- | Env.v | 3249 | logplain |
| -rw-r--r-- | EnvRing.v | 31977 | logplain |
| -rw-r--r-- | Fourier.v | 129 | logplain |
| -rw-r--r-- | Fourier_util.v | 699 | logplain |
| -rw-r--r-- | Lia.v | 1673 | logplain |
| -rw-r--r-- | Lqa.v | 2183 | logplain |
| -rw-r--r-- | Lra.v | 2247 | logplain |
| -rw-r--r-- | MExtraction.v | 2844 | logplain |
| -rw-r--r-- | OrderedRing.v | 14270 | logplain |
| -rw-r--r-- | Psatz.v | 2208 | logplain |
| -rw-r--r-- | QMicromega.v | 7357 | logplain |
| -rw-r--r-- | RMicromega.v | 13077 | logplain |
| -rw-r--r-- | Refl.v | 4254 | logplain |
| -rw-r--r-- | RingMicromega.v | 34697 | logplain |
| -rw-r--r-- | Tauto.v | 39855 | logplain |
| -rw-r--r-- | VarMap.v | 2891 | logplain |
| -rw-r--r-- | ZCoeff.v | 5561 | logplain |
| -rw-r--r-- | ZMicromega.v | 49011 | logplain |
| -rw-r--r-- | Zify.v | 1016 | logplain |
| -rw-r--r-- | ZifyBool.v | 7926 | logplain |
| -rw-r--r-- | ZifyClasses.v | 9417 | logplain |
| -rw-r--r-- | ZifyComparison.v | 2535 | logplain |
| -rw-r--r-- | ZifyInst.v | 14734 | logplain |
| -rw-r--r-- | ZifyPow.v | 25 | logplain |
| -rw-r--r-- | Ztac.v | 3607 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |