aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Expand)Author
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one c...Guillaume Melquiond
2019-07-09Merge PR #10471: [core] [api] Support OCaml 4.08Gaëtan Gilbert
2019-07-08[core] [api] Support OCaml 4.08Emilio 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-24Merge PR #10394: [ide] chop sentences taking into account QUOTATION tokenPierre-Marie Pédrot
2019-06-19[ide] chop sentences taking into account QUOTATION tokenEnrico Tassi
2019-06-18Merge PR #10398: Revert "Fix bug #5710"Pierre-Marie Pédrot
2019-06-18Revert "Fix bug #5710"Vincent Laporte
2019-06-17Update copyright years outside of headers.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-16Merge PR #10327: Fix bug #5710Pierre-Marie Pédrot
2019-06-15[dune] Install .byte version of coqidetop like for coqtop.Théo Zimmermann
2019-06-10Merge PR #9566: [proof] Move proofs that have an associated constant to `Lemmas`Pierre-Marie Pédrot
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-07Fix bug #5710Claude Stolze
2019-06-06Fix panel behavior as requested by #10292Claude Stolze
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-23Fixing typos - Part 2JPR
2019-05-14CoqIDE: Treat unknown arguments starting with dash as unknown options rather ...Hugo Herbelin
2019-05-11Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ...Pierre-Marie Pédrot
2019-05-07Merge PR #10063: CoqIDE: recognize qualified identifiers as words.Pierre-Marie Pédrot
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-05-03CoqIDE: recognize qualified identifiers as words.Jasper Hugunin
2019-04-30Renaming nanoPG to microPG.Hugo Herbelin
2019-04-30CoqIDE nanoPG: adding keys to go the start/end of file (w/o evaluating).Hugo Herbelin
2019-04-30NanoPG doc: telling that char, word, sentence, line have their unicode meaning.Hugo Herbelin
2019-04-30Cosmetic in nanoPG.ml: fixing a wrong indentation.Hugo Herbelin
2019-04-30CoqIDE: Adding MacOS X support for Meta-based nano-PG keys.Hugo Herbelin
2019-04-30NanoPG: expanding the notation C- and M- to Ctrl- and Meta-.Hugo Herbelin
2019-04-30Fix a nanoPG bug: was accepting unexpectedly extra modifier keys pressed.Hugo Herbelin
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...Maxime Dénès
2019-04-27CoqIDE, cosmetic: removing obsolete comments.Hugo Herbelin
2019-04-27CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899).Hugo Herbelin
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-25Fix PKG in ide/.merlin.in for gtk3Gaëtan Gilbert
2019-04-23[ide] update coq-ssreflect.lang wrt under tacticEnrico Tassi
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
2019-04-15[CoqIDE] Fix build system for macOSVincent Laporte
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-08Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Pierre-Marie Pédrot
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès