| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Notations.v | 357 | logplain |
| -rw-r--r-- | bug4076.v | 669 | logplain |
| -rw-r--r-- | bug4076bis.v | 729 | logplain |
| -rw-r--r-- | constructor.v | 16381 | logplain |
| -rw-r--r-- | evar_instance.v | 3879 | logplain |
| -rw-r--r-- | f_equal.v | 276 | logplain |
| -rw-r--r-- | guard.v | 523 | logplain |
| -rw-r--r-- | injection.v | 3567 | logplain |
| -rw-r--r-- | lettuple.v | 606 | logplain |
| -rw-r--r-- | pattern.v | 1235 | logplain |
| -rw-r--r-- | patternmatching.v | 1380 | logplain |
| -rw-r--r-- | pretyping.v | 128558 | logplain |
| -rw-r--r-- | ring.v | 235 | logplain |
| -rw-r--r-- | ring2.v | 1050 | logplain |
| -rw-r--r-- | setoid_rewrite.v | 196 | logplain |
| -rw-r--r-- | unification.v | 1433 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |