aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
Commit message (Expand)AuthorAge
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
* IDE: escape popup text (close: 3600)Gravatar Enrico Tassi2014-09-09
* Quick fix for avoiding infinitely many respawning and Warning "CoqGravatar Hugo Herbelin2014-08-12
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* CoqIDE: better error reporting for Qed on incomplete proofGravatar Enrico Tassi2014-03-26
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
* STM: tell the user if the master is recomputing states validated by workersGravatar Enrico Tassi2014-01-30
* CoqIDE: do not unfocus if not needed on errors (closes: 3197)Gravatar Enrico Tassi2014-01-06
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
* CoqIDE: show error message for parsing errorsGravatar Enrico Tassi2013-11-27
* CoqIDE: scroll to the right position if there is an interp errorGravatar gareuselesinge2013-10-31
* CoqIDE: fix coloring bug when jumping back to the first phraseGravatar gareuselesinge2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* CoqIDE: do not try to backtrack to a dummy idGravatar gareuselesinge2013-10-22
* CoqIDE: display in the errors window also the slaves statusGravatar gareuselesinge2013-10-22
* CoqIDE: error reporting fixedGravatar gareuselesinge2013-10-10
* CoqIDE: ported to DocumentGravatar gareuselesinge2013-10-10
* CoqIDE: move cmd_stack to a separate module: DocumentGravatar gareuselesinge2013-10-10
* CoqIDE: fix jumpig out of a focused proofGravatar gareuselesinge2013-10-07
* CoqIDE: cStack -> DocumentGravatar gareuselesinge2013-10-07
* CoqIDE: when checking the whole document, center script view on errorGravatar gareuselesinge2013-10-01
* CoqIDE: fixed advance_until wrt unfocusingGravatar gareuselesinge2013-10-01
* CoqIDE: do not print cmd_stack too oftenGravatar gareuselesinge2013-10-01
* CoqIDE: fix reset initialGravatar gareuselesinge2013-10-01
* CoqIDE: wg_Tooltip removed, new tooltip handlingGravatar gareuselesinge2013-09-30
* CoqIDE ported to the revides protocolGravatar gareuselesinge2013-09-30
* When Coq is reset-initialed by CoqIDE, do reset jobs countersGravatar gareuselesinge2013-09-13
* CoqIDE: new async error reporting window and slaves statusGravatar gareuselesinge2013-09-13
* CoqIDE: show number of proofs being checked in backgroundGravatar gareuselesinge2013-09-12
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
* Automatic backtracking if locked zone is editedGravatar gareuselesinge2013-08-11
* Adding the processed tag to comments in CoqIDE.Gravatar ppedrot2013-08-09
* Coqide ported to STMGravatar gareuselesinge2013-08-08
* Coqide: Globalization feedback (proof of concept)Gravatar gareuselesinge2013-04-25
* raise UnsafeSuccess -> feedback AddedAxiomGravatar gareuselesinge2013-04-25
* Coqide: new feedback mechanism for structured contentGravatar gareuselesinge2013-04-25
* Monadification of coqtop queries in CoqIDEGravatar ppedrot2013-01-26
* Uniformization of Coq tasksGravatar ppedrot2013-01-26
* Coqide: cleaner Coq.PrintOpt and session creationGravatar letouzey2012-12-19
* Coqide: allow editing even during a backtrackGravatar letouzey2012-12-11
* Coqide: restore the tag removal of copy-pasted zonesGravatar letouzey2012-12-10
* Coqide: some more refactoring to lighten coqide.mlGravatar letouzey2012-12-10