aboutsummaryrefslogtreecommitdiff
path: root/ide/idetop.ml
AgeCommit message (Expand)Author
2020-06-02Move CoqIDE to its own folderMaxime Dénès
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
2020-02-23Adding a Display Parentheses menu in CoqIDE.Hugo Herbelin
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-07-08[errors] Small cleanups and removal of dead code.Emilio Jesus Gallego Arias
2019-07-08Usage: bypassing a useless detour via a reference.Hugo Herbelin
2019-07-08An even more uniform treatment of the -help option across executables.Hugo Herbelin
2019-07-08Some common points between coqc and other coq binaries.Hugo Herbelin
2019-07-08Passing command-line option async_proofs_worker_priority functionally.Hugo Herbelin
2019-07-08Adding methods help and parse_extra to custom toplevels data.Hugo Herbelin
2019-06-27[vernac] Cleanup on interface of VernacentriesEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-14CoqIDE: Treat unknown arguments starting with dash as unknown options rather ...Hugo Herbelin
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...Maxime Dénès
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-01-27[ide] fail on unavailable commands before adding to the documentEnrico Tassi
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-12Merge PR #9101: Fix 8922 againHugo Herbelin
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-24[toplevel] Allow to specify default options.Emilio Jesus Gallego Arias
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
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-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-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-18Remove reference name type.Maxime Dénès
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:03:00 +0000