| 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 | 1674 | logplain |
| -rw-r--r-- | Lqa.v | 2186 | logplain |
| -rw-r--r-- | Lra.v | 2250 | 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 | 8701 | logplain |
| -rw-r--r-- | RMicromega.v | 15224 | logplain |
| -rw-r--r-- | Refl.v | 4254 | logplain |
| -rw-r--r-- | RingMicromega.v | 34697 | logplain |
| -rw-r--r-- | Tauto.v | 62474 | logplain |
| -rw-r--r-- | VarMap.v | 2891 | logplain |
| -rw-r--r-- | ZArith_hints.v | 2003 | logplain |
| -rw-r--r-- | ZCoeff.v | 5561 | logplain |
| -rw-r--r-- | ZMicromega.v | 50443 | logplain |
| -rw-r--r-- | Zify.v | 1096 | logplain |
| -rw-r--r-- | ZifyBool.v | 4602 | logplain |
| -rw-r--r-- | ZifyClasses.v | 9347 | logplain |
| -rw-r--r-- | ZifyComparison.v | 2575 | logplain |
| -rw-r--r-- | ZifyInst.v | 15000 | logplain |
| -rw-r--r-- | ZifyPow.v | 25 | logplain |
| -rw-r--r-- | Ztac.v | 3607 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |