aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | Fix #176.Gravatar Pierre Courtieu2017-04-19
| | | | | | | | | | | | | | | The code uses several token searcher and the wrong one was called somewhere.
* | | Add file contrib/mmm/.nosearch to help feature extraction toolsGravatar Jonas Bernoulli2017-04-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This change is intended as an intermediate step toward the removal of the bundled copy of `mmm' package. Even with this change, PG continues to use the bundled version, unless `mmm-auto' is already loaded at the time PG first loads `proof-auxmodes'. The benefit of this change is that tools that extract the features provided and required by a package, such as those used to maintain the Emacsmirror, will no longer be tricked into believing that `mmm' is part of PG. Eventually the bundled `mmm' copy should be removed completely, as I suggested in #171, and as was already on the roadmap before I did so.
* | | [doc]: add documentation for the EasyCrypt modeGravatar Pierre-Yves Strub2017-04-12
| | |
* | | Fixing #173.Gravatar Pierre Courtieu2017-03-31
| | |
* | | Added support for future new options (trunk).Gravatar Pierre Courtieu2017-03-22
| | |
* | | Fixing #167.Gravatar Pierre Courtieu2017-03-13
| | |
| | * extend helpspan, issue #158Gravatar Paul Steckler2017-03-09
| |/ |/|
| * elpa: Add a package file and a package.el-friendly init scriptGravatar Clément Pit--Claudel2017-03-08
| |
| * Add a FIXME in coq.elGravatar Clément Pit--Claudel2017-03-08
| |
| * Remove uses of defpgdefault in coq-abbrevGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | This file is `require'-d when compiling coq.el, and at that point the proof assistant isn't set to coq yet, so it would define variables prefixed by `nil-' instead of `coq'.
| * Remove uses of defpacustom in coq-compile-commonGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | This file is `require'-d from other places, at compile time. This doesn't work nicely with compilation by package.el (PG complains and says "defpacustom: Proof assistant setting compile-before-require re-defined!")
| * easycrypt: Don't require pg-custom: it breaks compilationGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | The problem is that loading pg-custom runs a bunch of defpgcustom, with no current proof assistant. Then when coq or easycrypt calls proof-ready-for-assistant, pg-custom isn't loaded again.
| * Remove compile-time calls to proof-ready-for-assistantGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el.
| * Remove unnecessary calls to 'eval-and-compile'Gravatar Clément Pit--Claudel2017-03-08
| |
| * Remove a few useless eval-and-compile callsGravatar Clément Pit--Claudel2017-03-08
| |
| * Remove some Emacs <24.1 compatibility cruftGravatar Clément Pit--Claudel2017-03-08
| |
| * Fix incorrect uses of defvarGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | | | It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance.
| * Fix incorrect assumption that noninteractive == byte-compilingGravatar Clément Pit--Claudel2017-03-08
|/ | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
* Merge commit '06fd76163b857a056ac44e7437efa17656f06e5b'Gravatar Paul Steckler2017-03-08
|\
| * Fixing unicode tokens in generic code and in coq.Gravatar Pierre Courtieu2017-03-08
| |
* | get threeb frames only when neededGravatar Paul Steckler2017-03-06
| |
* | one more redundant call removedGravatar Paul Steckler2017-03-06
| |
* | remove redundant calls, simplify codeGravatar Paul Steckler2017-03-06
| |
* | Merge pull request #163 from ProofGeneral/fix_indentationGravatar Pierre Courtieu2017-03-03
|\ \ | | | | | | Fix indentation
* | | 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
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:38:15 +0000