aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
Commit message (Expand)AuthorAge
* Removing a warning in CoqOps.Gravatar Pierre-Marie Pédrot2015-09-15
* CoqIDE: recenter on backtrack (Close: #4277)Gravatar Enrico Tassi2015-07-11
* Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Gravatar Hugo Herbelin2015-06-16
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
* CoqIDE: fix tag colors to support superposing unsafe and partialGravatar Enrico Tassi2015-03-11
* CoqIDE: do not lose tag on Qed ending focused proofGravatar Enrico Tassi2015-03-11
* CoqIDE: correclty unfocus (remove all tags) when jumping out of a proofGravatar Enrico Tassi2015-02-25
* Fixing bug #4037.Gravatar Pierre-Marie Pédrot2015-02-15
* Made the CoqIDE progress gutter clickable.Gravatar Pierre-Marie Pédrot2015-01-29
* Update headers.Gravatar Maxime Dénès2015-01-12
* Implementing a segment-viewer in CoqIDE.Gravatar Pierre-Marie Pédrot2015-01-05
* CoqIDE: better messagesGravatar Enrico Tassi2014-12-17
* 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