| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | analyze.ml | 11810 | logplain |
| -rw-r--r-- | analyze.mli | 1336 | logplain |
| -rw-r--r-- | check.ml | 16274 | logplain |
| -rw-r--r-- | check.mli | 1138 | logplain |
| -rw-r--r-- | check.mllib | 103 | logplain |
| -rw-r--r-- | checkInductive.ml | 7595 | logplain |
| -rw-r--r-- | checkInductive.mli | 981 | logplain |
| -rw-r--r-- | checkTypes.ml | 1502 | logplain |
| -rw-r--r-- | checkTypes.mli | 859 | logplain |
| -rw-r--r-- | check_stat.ml | 1816 | logplain |
| -rw-r--r-- | check_stat.mli | 765 | logplain |
| -rw-r--r-- | checker.ml | 14797 | logplain |
| -rw-r--r-- | checker.mli | 701 | logplain |
| -rw-r--r-- | coqchk.ml | 26 | logplain |
| -rw-r--r-- | coqchk.mli | 808 | logplain |
| -rw-r--r-- | dune | 619 | logplain |
| -rw-r--r-- | include | 4917 | logplain |
| -rw-r--r-- | mod_checking.ml | 5913 | logplain |
| -rw-r--r-- | mod_checking.mli | 843 | logplain |
| -rw-r--r-- | safe_checking.ml | 1255 | logplain |
| -rw-r--r-- | safe_checking.mli | 919 | logplain |
| -rw-r--r-- | validate.ml | 5389 | logplain |
| -rw-r--r-- | validate.mli | 726 | logplain |
| -rw-r--r-- | values.ml | 10816 | logplain |
| -rw-r--r-- | values.mli | 1598 | logplain |
| -rw-r--r-- | votour.ml | 11829 | logplain |
| -rw-r--r-- | votour.mli | 808 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |