aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-02use Utf8 from Coq libraryPaul Steckler
2017-02-27serveral coqtags fixes and improvementsHendrik Tews
- precise tags for definitions - fix bug with nonempty white space lines - add several keywords (Proposition, Record, ...) - generate tags for constructors of inductive definitions and for record labels
2017-02-27Merge pull request #156 from Matafou/fix-154Pierre Courtieu
Fixing #154.
2017-02-25Add easycrypt and twelf to MakefileClément Pit--Claudel
2017-02-24Removing spurious debug messages.Pierre Courtieu
2017-02-23Fixing #154.Pierre Courtieu
2017-02-21[ec mode]: update keywordsPierre-Yves Strub
2017-01-19save settings not defined with defpacustom (fixes #142)Hendrik Tews
- infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
2017-01-18split emergency-cleanup to handle interrupts properly (fixes #143)Hendrik Tews
Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors.
2017-01-17move phox from main to obscure instancesHendrik Tews
see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working...
2017-01-17use makeinfo instead of texi2htmlHendrik Tews
texi2html is dead, see for instance https://wiki.debian.org/Texi2htmlTransition
2017-01-17fix coqtagsHendrik Tews
@psteckler I believe you have this patch already in your branch.
2017-01-17Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106)Jason Gross
2017-01-17Merge pull request #44 from EasyCrypt/masterhendriktews
EasyCrypt PG mode
2017-01-17Merge pull request #107 from JasonGross/patch-3hendriktews
Add Context to coq-syntax.el
2017-01-17fix icon installation and add 64 and 128 square icons (fixes #141)Hendrik Tews
2017-01-14Fix prooftree for Coq 8.6Hendrik Tews
In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
2017-01-04Merge remote-tracking branch 'OFFICIAL/master'Pierre Courtieu
2017-01-04Fixing #121 + avoid hiding user windows too much.Pierre Courtieu
2016-12-31A first pass at converting from CVS to git. (#127)zhenya1007
Do some cleanup in the Makefile.devel file.
2016-12-31add second argument to looking-back, required in emacs25Hendrik Tews
2016-12-28fix prooftree crash with long evar linesHendrik Tews
2016-12-28properly reset the vio2vo delay timerHendrik Tews
cancel-timer does of course not set the variable that holds the timer to nil
2016-12-26Fix doc for Coq electric terminator.Erik Martin-Dorel
Close ProofGeneral/PG#138.
2016-12-16Merge pull request #133 from hendriktews/file-errorhendriktews
die gracefully when visiting files in nonexisting directories
2016-12-15add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576Hendrik Tews
2016-12-15Improve doc on coq project fileHendrik Tews
... following the discussion in github on 32fea19d1bb66593e469b1a8e6ad38f3ae1714bf
2016-12-15fix :get for coq-search-blacklistHendrik Tews
2016-12-15Merge pull request #101 from tchajed/print-universes-optionhendriktews
Add Set Printing Universes to options menu
2016-12-15die gracefully when visiting files in nonexisting directoriesHendrik Tews
2016-12-14fix generic interrupt procedure to interrupt parallel background compilationHendrik Tews
2016-12-14fix race in vio2vo compilation startHendrik Tews
2016-12-14fix parallel build and other issues in Makefile (fixes #130)Hendrik Tews
2016-12-14Merge pull request #129 from hendriktews/keep-goinghendriktews
Keep going
2016-12-14Merge pull request #132 from Matafou/masterPierre Courtieu
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
2016-12-13Same name guessing for coqc/coqdep then for coqtop.Pierre Courtieu
2016-12-12remove default absolute name from coq-prog-name, but keep dipsplaying it ↵Pierre Courtieu
when asking for it.
2016-12-08documentation and CHANGES for coq-compile-keep-goingHendrik Tews
2016-12-08option coq-compile-keep-going for parallel compilationHendrik Tews
With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error.
2016-12-02remove ancestor hash in Coq parallel background compilationHendrik Tews
2016-11-30fix customize-group coqHendrik Tews
2016-11-30fix 2 compilation warnings (fixes #33)Hendrik Tews
2016-11-30style change: use when for if coq-debug-auto-compilationHendrik Tews
2016-11-30Merge pull request #125 from hendriktews/quickhendriktews
support for quick compilation
2016-11-30use coq-- for internal compilation variablesHendrik Tews
2016-11-30write CHANGESHendrik Tews
2016-11-30next-error support for vio2vo error messagesHendrik Tews
2016-11-29update documentationHendrik Tews
2016-11-29delay vio2vo compilationHendrik Tews
... to make it less likely people run into the library inconsistency issue with vio2vo
2016-11-298.4 compatibility for quick supportHendrik Tews
8.4 compatibility is done by ignoring all quick settings for `coq-compile-quick' via a :set function. This does only work if this variable is only changed via the customization system and not directly via setq.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:00:01 +0000