| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Berardi.v | 4223 | logplain |
| -rwxr-xr-x | Classical.v | 622 | logplain |
| -rwxr-xr-x | Classical_Pred_Set.v | 1699 | logplain |
| -rwxr-xr-x | Classical_Pred_Type.v | 1710 | logplain |
| -rwxr-xr-x | Classical_Prop.v | 1900 | logplain |
| -rwxr-xr-x | Classical_Type.v | 632 | logplain |
| -rw-r--r-- | Decidable.v | 1741 | logplain |
| -rw-r--r-- | Elimdep.v | 731 | logplain |
| -rwxr-xr-x | Eqdep.v | 2679 | logplain |
| -rw-r--r-- | Eqdep_dec.v | 3712 | logplain |
| -rw-r--r-- | JMeq.v | 1553 | logplain |
| -rwxr-xr-x | intro.tex | 247 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |