| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | compat.v | 1495 | logplain |
| -rw-r--r-- | constr.v | 365 | logplain |
| -rw-r--r-- | errors.v | 269 | logplain |
| -rw-r--r-- | example1.v | 572 | logplain |
| -rw-r--r-- | example2.v | 4001 | logplain |
| -rw-r--r-- | ltac2env.v | 541 | logplain |
| -rw-r--r-- | matching.v | 1723 | logplain |
| -rw-r--r-- | notations.v | 414 | logplain |
| -rw-r--r-- | quot.v | 656 | logplain |
| -rw-r--r-- | rebind.v | 479 | logplain |
| d--------- | stuff | 35 | logplain |
| -rw-r--r-- | tacticals.v | 516 | logplain |
| -rw-r--r-- | term_notations.v | 545 | logplain |
| -rw-r--r-- | typing.v | 1205 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |