| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-08 | Fixing unicode tokens in generic code and in coq. | Pierre Courtieu | |
| 2017-03-06 | get threeb frames only when needed | Paul Steckler | |
| 2017-03-06 | one more redundant call removed | Paul Steckler | |
| 2017-03-06 | remove redundant calls, simplify code | Paul Steckler | |
| 2017-03-03 | Merge pull request #163 from ProofGeneral/fix_indentation | Pierre Courtieu | |
| Fix indentation | |||
| 2017-03-03 | Refreshing goal when Set Printing xxx. (#162) | Pierre Courtieu | |
| * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open). | |||
| 2017-03-03 | Remove default key-binding for proof-electric-terminator-toggle. | Erik Martin-Dorel | |
| Close ProofGeneral/PG#160 | |||
| 2017-03-02 | use Utf8 from Coq library | Paul Steckler | |
| 2017-02-27 | serveral coqtags fixes and improvements | Hendrik 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-27 | Merge pull request #156 from Matafou/fix-154 | Pierre Courtieu | |
| Fixing #154. | |||
| 2017-02-25 | Add easycrypt and twelf to Makefile | Clément Pit--Claudel | |
| 2017-02-24 | Removing spurious debug messages. | Pierre Courtieu | |
| 2017-02-23 | Fixing #154. | Pierre Courtieu | |
| 2017-02-21 | [ec mode]: update keywords | Pierre-Yves Strub | |
| 2017-01-26 | Fixing #147 and #91 + others indentation bugs. | Pierre Courtieu | |
| 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. | |||
| 2017-01-26 | Merge branch 'master' of github.com:ProofGeneral/PG into master_origin | Pierre Courtieu | |
| 2017-01-24 | annoying missing parentheisis in a comment. | Pierre Courtieu | |
| 2017-01-19 | save 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-18 | split 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-17 | move phox from main to obscure instances | Hendrik Tews | |
| see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working... | |||
| 2017-01-17 | use makeinfo instead of texi2html | Hendrik Tews | |
| texi2html is dead, see for instance https://wiki.debian.org/Texi2htmlTransition | |||
| 2017-01-17 | fix coqtags | Hendrik Tews | |
| @psteckler I believe you have this patch already in your branch. | |||
| 2017-01-17 | Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106) | Jason Gross | |
| 2017-01-17 | Merge pull request #44 from EasyCrypt/master | hendriktews | |
| EasyCrypt PG mode | |||
| 2017-01-17 | Merge pull request #107 from JasonGross/patch-3 | hendriktews | |
| Add Context to coq-syntax.el | |||
| 2017-01-17 | fix icon installation and add 64 and 128 square icons (fixes #141) | Hendrik Tews | |
| 2017-01-14 | Fix prooftree for Coq 8.6 | Hendrik 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-04 | Merge remote-tracking branch 'OFFICIAL/master' | Pierre Courtieu | |
| 2017-01-04 | Fixing #121 + avoid hiding user windows too much. | Pierre Courtieu | |
| 2016-12-31 | A first pass at converting from CVS to git. (#127) | zhenya1007 | |
| Do some cleanup in the Makefile.devel file. | |||
| 2016-12-31 | add second argument to looking-back, required in emacs25 | Hendrik Tews | |
| 2016-12-28 | fix prooftree crash with long evar lines | Hendrik Tews | |
| 2016-12-28 | properly reset the vio2vo delay timer | Hendrik Tews | |
| cancel-timer does of course not set the variable that holds the timer to nil | |||
| 2016-12-26 | Fix doc for Coq electric terminator. | Erik Martin-Dorel | |
| Close ProofGeneral/PG#138. | |||
| 2016-12-16 | Merge pull request #133 from hendriktews/file-error | hendriktews | |
| die gracefully when visiting files in nonexisting directories | |||
| 2016-12-15 | add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576 | Hendrik Tews | |
| 2016-12-15 | Improve doc on coq project file | Hendrik Tews | |
| ... following the discussion in github on 32fea19d1bb66593e469b1a8e6ad38f3ae1714bf | |||
| 2016-12-15 | fix :get for coq-search-blacklist | Hendrik Tews | |
| 2016-12-15 | Merge pull request #101 from tchajed/print-universes-option | hendriktews | |
| Add Set Printing Universes to options menu | |||
| 2016-12-15 | die gracefully when visiting files in nonexisting directories | Hendrik Tews | |
| 2016-12-14 | fix generic interrupt procedure to interrupt parallel background compilation | Hendrik Tews | |
| 2016-12-14 | fix race in vio2vo compilation start | Hendrik Tews | |
| 2016-12-14 | fix parallel build and other issues in Makefile (fixes #130) | Hendrik Tews | |
| 2016-12-14 | Merge pull request #129 from hendriktews/keep-going | hendriktews | |
| Keep going | |||
| 2016-12-14 | Merge pull request #132 from Matafou/master | Pierre Courtieu | |
| Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying… | |||
| 2016-12-13 | Same name guessing for coqc/coqdep then for coqtop. | Pierre Courtieu | |
| 2016-12-12 | remove default absolute name from coq-prog-name, but keep dipsplaying it ↵ | Pierre Courtieu | |
| when asking for it. | |||
| 2016-12-08 | documentation and CHANGES for coq-compile-keep-going | Hendrik Tews | |
| 2016-12-08 | option coq-compile-keep-going for parallel compilation | Hendrik 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-02 | remove ancestor hash in Coq parallel background compilation | Hendrik Tews | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |