aboutsummaryrefslogtreecommitdiff
path: root/coq/coq-syntax.el
AgeCommit message (Expand)Author
2021-04-16add feature to omit complete opaque proofsHendrik Tews
2021-03-21Fix #562. Lazy/multi_?match indentation support.Pierre Courtieu
2020-11-19coq: Add highlighting for Hint ModeClément Pit-Claudel
2020-10-14Highlight ComputeLi-yao Xia
2020-06-15Add coloration for Ltac2 commandsCyril Anaclet
2020-05-29fix: backtrack wrong type argumentAnaclet
2020-05-29Apply reviews of @erikmdCyril Anaclet
2020-05-29WIP for #487Cyril Anaclet
2020-05-29Fix name clash & rephrase some stringsErik Martin-Dorel
2020-05-29All case for Show and regex variableCyril Anaclet
2020-05-28Added a few coq commands.Pierre Courtieu
2020-04-02Merge pull request #474 from tchajed/add-ltac2-syntaxErik Martin-Dorel
2020-04-02Add support for core Ltac2 syntaxTej Chajed
2020-04-01SearchAbout is deprecated since 8.5; use Search insteadClément Pit-Claudel
2019-12-08fix: Recognize "Timeout" before save keywordsErik Martin-Dorel
2018-12-26Make coq-mode work without generic/proof-*Stefan Monnier
2018-12-22* coq-mode.el: New file to make coq-mode independent from PGStefan Monnier
2018-12-15Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Stefan Monnier
2018-12-14Fix remaining uses of CL; Make files more declarativeStefan Monnier
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-08-17Support the Variant vernacularTej Chajed
2018-06-15Fixing last commit.Pierre Courtieu
2018-06-15Fix #368 (emacs < 25 split-string has no trim arg).Pierre Courtieu
2018-06-13Fix multiple hyp overlays.Pierre Courtieu
2018-06-13Fix the fix #355.Pierre Courtieu
2018-06-08Changed the look of folding/unfolding hyps.Pierre Courtieu
2018-06-06Small fix in a regexp.Pierre Courtieu
2018-06-04Shorter CHANGES + smal fixes in hide/highlight hyps code.Pierre Courtieu
2018-06-01Click hypothesis to (un)hide them.Pierre Courtieu
2018-05-31Infrastructure for transient hyps highlighting.Pierre Courtieu
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2018-02-07typo in abbrevs.Pierre Courtieu
2017-05-05Merge pull request #157 from ProofGeneral/elpaClément Pit-Claudel
2017-04-25Typo from commit 758e679e.Pierre Courtieu
2017-04-24Preparing new warning tags (no more special chars).Pierre Courtieu
2017-03-31Fixing #173.Pierre Courtieu
2017-03-22Added support for future new options (trunk).Pierre Courtieu
2017-03-08Fix incorrect uses of defvarClément Pit--Claudel
2017-01-17Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106)Jason Gross
2017-01-17Merge pull request #107 from JasonGross/patch-3hendriktews
2016-10-28fix coq-require-command-regexp (fixes #75)Hendrik Tews
2016-09-01Add Context to coq-syntax.elJason Gross
2016-08-14Add Reserved Infix like Reserved Notation (#95)Jason Gross
2016-07-22Adding the option to highlight susual symbols.Pierre Courtieu
2016-07-03Highlight Existing Class like Existing Instance (#85)Jason Gross
2016-07-01Highlight [nra] like [nia] and [lia] and [lra] (#84)Jason Gross
2016-06-10Color lia, romega, nia, psatz, nsatz, lraJason Gross
2016-06-08abbrev twivking.Pierre Courtieu
2016-06-08Fixing font-locking of unicode forall etc.Pierre Courtieu
2016-05-27Fixing a smal glitch in indentation.Pierre Courtieu