| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | DeclConstant.v | 2823 | logplain |
| -rw-r--r-- | Env.v | 3249 | logplain |
| -rw-r--r-- | EnvRing.v | 31591 | logplain |
| -rw-r--r-- | Fourier.v | 129 | logplain |
| -rw-r--r-- | Fourier_util.v | 699 | logplain |
| -rw-r--r-- | Lia.v | 1676 | logplain |
| -rw-r--r-- | Lqa.v | 2186 | logplain |
| -rw-r--r-- | Lra.v | 2219 | 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 | 7309 | logplain |
| -rw-r--r-- | RMicromega.v | 12642 | logplain |
| -rw-r--r-- | Refl.v | 4254 | logplain |
| -rw-r--r-- | RingMicromega.v | 33998 | logplain |
| -rw-r--r-- | Tauto.v | 39491 | logplain |
| -rw-r--r-- | VarMap.v | 2720 | logplain |
| -rw-r--r-- | ZCoeff.v | 5561 | logplain |
| -rw-r--r-- | ZMicromega.v | 48711 | 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 |