aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | Refreshing goal when Set Printing xxx. (#162)Gravatar Pierre Courtieu2017-03-03
| | | | | | | | | | | | | | | * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open).
* | | Remove default key-binding for proof-electric-terminator-toggle.Gravatar Erik Martin-Dorel2017-03-03
| | | | | | | | | | | | Close ProofGeneral/PG#160
* | | use Utf8 from Coq libraryGravatar Paul Steckler2017-03-02
| | |
* | | serveral coqtags fixes and improvementsGravatar Hendrik Tews2017-02-27
| | | | | | | | | | | | | | | | | | | | | | | | - 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
* | | Merge pull request #156 from Matafou/fix-154Gravatar Pierre Courtieu2017-02-27
|\ \ \ | | | | | | | | Fixing #154.
* | | | Add easycrypt and twelf to MakefileGravatar Clément Pit--Claudel2017-02-25
| | | |
| * | | Removing spurious debug messages.Gravatar Pierre Courtieu2017-02-24
| | | |
| * | | Fixing #154.Gravatar Pierre Courtieu2017-02-23
|/ / /
* | / [ec mode]: update keywordsGravatar Pierre-Yves Strub2017-02-21
| |/ |/|
| * Fixing #147 and #91 + others indentation bugs.Gravatar Pierre Courtieu2017-01-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | While fixing these I discovered several flaws in indentation (what a suprise). The probem is the following: since we don't have a precise grammar of tactics, smie often decides that the parent of a sub-part of a tactic is the previous command instead of the current tacic. Typical example (fixed now but in general): foo. apply bar with bar'. Since "apply ... bar'" is considered as one leaf of the grammar, it is considered to be a child of the previous dot. . /\ / \ foo apply...bar' Therefore indentation of "with" wants to align with parent "." and hence with "foo". Basically we should try to define a much more precise grammar of complex tactics (with with, as, using etc) in order to fix the problem. Of course this has the drawback of making impossible to support user tactic notations.
| * Merge branch 'master' of github.com:ProofGeneral/PG into master_originGravatar Pierre Courtieu2017-01-26
| |\ | |/ |/|
| * annoying missing parentheisis in a comment.Gravatar Pierre Courtieu2017-01-24
| |
* | save settings not defined with defpacustom (fixes #142)Gravatar Hendrik Tews2017-01-19
| | | | | | | | | | | | | | - infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
* | split emergency-cleanup to handle interrupts properly (fixes #143)Gravatar Hendrik Tews2017-01-18
| | | | | | | | | | | | Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors.
* | move phox from main to obscure instancesGravatar Hendrik Tews2017-01-17
| | | | | | | | | | see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working...
* | use makeinfo instead of texi2htmlGravatar Hendrik Tews2017-01-17
| | | | | | | | | | texi2html is dead, see for instance https://wiki.debian.org/Texi2htmlTransition
* | fix coqtagsGravatar Hendrik Tews2017-01-17
| | | | | | | | @psteckler I believe you have this patch already in your branch.
* | Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106)Gravatar Jason Gross2017-01-17
| |
* | Merge pull request #44 from EasyCrypt/masterGravatar hendriktews2017-01-17
|\ \ | | | | | | EasyCrypt PG mode
* \ \ Merge pull request #107 from JasonGross/patch-3Gravatar hendriktews2017-01-17
|\ \ \ | | | | | | | | Add Context to coq-syntax.el
* | | | fix icon installation and add 64 and 128 square icons (fixes #141)Gravatar Hendrik Tews2017-01-17
| | | |
* | | | Fix prooftree for Coq 8.6Gravatar Hendrik Tews2017-01-14
| |_|/ |/| | | | | | | | | | | | | | | | | 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.
* | | Merge remote-tracking branch 'OFFICIAL/master'Gravatar Pierre Courtieu2017-01-04
|\ \ \
* | | | Fixing #121 + avoid hiding user windows too much.Gravatar Pierre Courtieu2017-01-04
| | | |
| * | | A first pass at converting from CVS to git. (#127)Gravatar zhenya10072016-12-31
| | | | | | | | | | | | Do some cleanup in the Makefile.devel file.
| * | | add second argument to looking-back, required in emacs25Gravatar Hendrik Tews2016-12-31
| | | |
| * | | fix prooftree crash with long evar linesGravatar Hendrik Tews2016-12-28
| | | |
| * | | properly reset the vio2vo delay timerGravatar Hendrik Tews2016-12-28
| | | | | | | | | | | | | | | | | | | | cancel-timer does of course not set the variable that holds the timer to nil
| * | | Fix doc for Coq electric terminator.Gravatar Erik Martin-Dorel2016-12-26
| | | | | | | | | | | | | | | | Close ProofGeneral/PG#138.
| * | | Merge pull request #133 from hendriktews/file-errorGravatar hendriktews2016-12-16
| |\ \ \ | | | | | | | | | | die gracefully when visiting files in nonexisting directories
| * | | | add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576Gravatar Hendrik Tews2016-12-15
| | | | |
| * | | | Improve doc on coq project fileGravatar Hendrik Tews2016-12-15
| | | | | | | | | | | | | | | | | | | | ... following the discussion in github on 32fea19d1bb66593e469b1a8e6ad38f3ae1714bf
| * | | | fix :get for coq-search-blacklistGravatar Hendrik Tews2016-12-15
| | | | |
| * | | | Merge pull request #101 from tchajed/print-universes-optionGravatar hendriktews2016-12-15
| |\ \ \ \ | | | | | | | | | | | | Add Set Printing Universes to options menu
| | | * | | die gracefully when visiting files in nonexisting directoriesGravatar Hendrik Tews2016-12-15
| | |/ / / | |/| | |
| * | | | fix generic interrupt procedure to interrupt parallel background compilationGravatar Hendrik Tews2016-12-14
| | | | |
| * | | | fix race in vio2vo compilation startGravatar Hendrik Tews2016-12-14
| | | | |
| * | | | fix parallel build and other issues in Makefile (fixes #130)Gravatar Hendrik Tews2016-12-14
| | | | |
| * | | | Merge pull request #129 from hendriktews/keep-goingGravatar hendriktews2016-12-14
|/| | | | | | | | | | | | | | Keep going
* | | | | Merge pull request #132 from Matafou/masterGravatar Pierre Courtieu2016-12-14
|\ \ \ \ \ | | | | | | | | | | | | Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
| * | | | | Same name guessing for coqc/coqdep then for coqtop.Gravatar Pierre Courtieu2016-12-13
| | | | | |
| * | | | | remove default absolute name from coq-prog-name, but keep dipsplaying it ↵Gravatar Pierre Courtieu2016-12-12
| | | | | | | | | | | | | | | | | | | | | | | | when asking for it.
| | * | | | documentation and CHANGES for coq-compile-keep-goingGravatar Hendrik Tews2016-12-08
| | | | | |
| | * | | | option coq-compile-keep-going for parallel compilationGravatar Hendrik Tews2016-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error.
| | * | | | remove ancestor hash in Coq parallel background compilationGravatar Hendrik Tews2016-12-02
| |/ / / / |/| | | |
* | | | | fix customize-group coqGravatar Hendrik Tews2016-11-30
| | | | |
* | | | | fix 2 compilation warnings (fixes #33)Gravatar Hendrik Tews2016-11-30
| | | | |
* | | | | style change: use when for if coq-debug-auto-compilationGravatar Hendrik Tews2016-11-30
| | | | |
* | | | | Merge pull request #125 from hendriktews/quickGravatar hendriktews2016-11-30
|\ \ \ \ \ | |/ / / / |/| | | | support for quick compilation
| * | | | use coq-- for internal compilation variablesGravatar Hendrik Tews2016-11-30
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 13:58:55 +0000