| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | .cvsignore | 14 | logplain |
| -rw-r--r-- | coq_fix_code.c | 5160 | logplain |
| -rw-r--r-- | coq_fix_code.h | 1146 | logplain |
| -rw-r--r-- | coq_gc.h | 2115 | logplain |
| -rw-r--r-- | coq_instruct.h | 1661 | logplain |
| -rw-r--r-- | coq_interp.c | 20042 | logplain |
| -rw-r--r-- | coq_interp.h | 919 | logplain |
| -rw-r--r-- | coq_memory.c | 7519 | logplain |
| -rw-r--r-- | coq_memory.h | 2073 | logplain |
| -rw-r--r-- | coq_values.c | 2168 | logplain |
| -rw-r--r-- | coq_values.h | 961 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |