| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | clenv.ml | 26552 | logplain |
| -rw-r--r-- | clenv.mli | 6993 | logplain |
| -rw-r--r-- | clenvtac.ml | 5068 | logplain |
| -rw-r--r-- | clenvtac.mli | 1183 | logplain |
| -rw-r--r-- | doc.tex | 424 | logplain |
| -rw-r--r-- | dune | 178 | logplain |
| -rw-r--r-- | evar_refiner.ml | 2696 | logplain |
| -rw-r--r-- | evar_refiner.mli | 912 | logplain |
| -rw-r--r-- | goal.ml | 5149 | logplain |
| -rw-r--r-- | goal.mli | 2831 | logplain |
| -rw-r--r-- | goal_select.ml | 2525 | logplain |
| -rw-r--r-- | goal_select.mli | 1225 | logplain |
| -rw-r--r-- | logic.ml | 22851 | logplain |
| -rw-r--r-- | logic.mli | 2604 | logplain |
| -rw-r--r-- | miscprint.ml | 2720 | logplain |
| -rw-r--r-- | miscprint.mli | 1244 | logplain |
| -rw-r--r-- | proof.ml | 18798 | logplain |
| -rw-r--r-- | proof.mli | 8167 | logplain |
| -rw-r--r-- | proof_bullet.ml | 7134 | logplain |
| -rw-r--r-- | proof_bullet.mli | 2018 | logplain |
| -rw-r--r-- | proofs.mllib | 103 | logplain |
| -rw-r--r-- | refine.ml | 5335 | logplain |
| -rw-r--r-- | refine.mli | 1834 | logplain |
| -rw-r--r-- | refiner.ml | 10017 | logplain |
| -rw-r--r-- | refiner.mli | 4520 | logplain |
| -rw-r--r-- | tacmach.ml | 6027 | logplain |
| -rw-r--r-- | tacmach.mli | 5039 | logplain |
| -rw-r--r-- | tactypes.ml | 2320 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |