| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | analyze.ml | 13228 | logplain |
| -rw-r--r-- | analyze.mli | 1376 | logplain |
| -rw-r--r-- | check.ml | 16255 | logplain |
| -rw-r--r-- | check.mli | 1138 | logplain |
| -rw-r--r-- | check.mllib | 103 | logplain |
| -rw-r--r-- | checkInductive.ml | 8977 | logplain |
| -rw-r--r-- | checkInductive.mli | 981 | logplain |
| -rw-r--r-- | checkTypes.ml | 1502 | logplain |
| -rw-r--r-- | checkTypes.mli | 863 | logplain |
| -rw-r--r-- | check_stat.ml | 3084 | logplain |
| -rw-r--r-- | check_stat.mli | 765 | logplain |
| -rw-r--r-- | checker.ml | 14894 | 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 | 637 | logplain |
| -rw-r--r-- | include | 4917 | logplain |
| -rw-r--r-- | mod_checking.ml | 6148 | logplain |
| -rw-r--r-- | mod_checking.mli | 829 | logplain |
| -rw-r--r-- | safe_checking.ml | 1255 | logplain |
| -rw-r--r-- | safe_checking.mli | 919 | logplain |
| -rw-r--r-- | validate.ml | 7042 | logplain |
| -rw-r--r-- | validate.mli | 767 | logplain |
| -rw-r--r-- | values.ml | 12105 | logplain |
| -rw-r--r-- | values.mli | 1613 | logplain |
| -rw-r--r-- | votour.ml | 11928 | logplain |
| -rw-r--r-- | votour.mli | 808 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |