aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Expand)Author
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-161) Make the diff setting a persistent settting.Jim Fehrle
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-27Merge PR #8166: Fix Search query in CoqIDE.Enrico Tassi
2018-07-26Fix Search query in CoqIDE.Pierre-Marie Pédrot
2018-07-26Expose the diff printing option as an UI entry in CoqIDE.Pierre-Marie Pédrot
2018-07-26Do not set diff printing on by default in CoqIDE.Pierre-Marie Pédrot
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-18Merge PR #7897: Remove fourier pluginEnrico Tassi
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-14[build] Build Coq and plugins with `-strict-sequence`Emilio Jesus Gallego Arias
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-03Remove unused arguments to Ide_slave.concl_next_tac.Gaëtan Gilbert
2018-06-27CoqIDE scrolls the proof buffer down to the first goal.Cyprien Mangin
2018-06-18Remove reference name type.Maxime Dénès
2018-05-28Merge PR #7419: Remove 100 occurrences of Evd.emptyPierre-Marie Pédrot
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-16[ide] Don't set `quiet` on start.Emilio Jesus Gallego Arias
2018-05-15Merge PR #7224: Attempt to fix the doubly encapsulated Ltac errors in coqideEnrico Tassi
2018-04-19[toplevel] let toploop_init change Coq optionsEnrico Tassi
2018-04-12Merge PR #7096: coqide: avoid marking sentences that are not in the document ...Pierre-Marie Pédrot
2018-04-12Attempt to fix the doubly encapsulated Ltac errors in coqide.Hugo Herbelin
2018-04-05Remove unused script.Théo Zimmermann
2018-03-28coqide: avoid marking sentences that are not in the document anymoreEnrico Tassi
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Merge PR #6923: Export optionsMaxime Dénès
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-09Export the various option localities in the API.Pierre-Marie Pédrot
2018-03-08coqide: queries from the query window are routed there (fix #5684)Enrico Tassi
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-19Merge PR #6753: [toplevel] Make toplevel state into a record.Maxime Dénès
2018-02-19Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Maxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-02-15[ide] Localize a IDE-specific flag.Emilio Jesus Gallego Arias
2018-02-09[toplevel] Refactor command line argument handling.Emilio Jesus Gallego Arias
2018-01-26allow vernacular controls before focus selector, issue #6587Paul Steckler
2018-01-22Merge PR #6625: Update location on tab switch, issue 6624Maxime Dénès
2018-01-19update location on tab switch, issue 6624Paul Steckler
2018-01-18add flash infos about wrap, not found, no. of replacements, no. of finds, iss...Paul Steckler
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès