| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-31 | STM: reorganize code and file names | Enrico Tassi | |
| - proofworkertop to deal with proof tasks - tacworkertop to deal with par: tactics - queryworkertop to deal with queries (next commit) | |||
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-06-25 | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi | |
| User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |