| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-26 | look for vernac controls before focus bracket, fix for #223 | Paul Steckler | |
| 2018-01-15 | Experimental fix for #220. | Pierre Courtieu | |
| 2017-12-11 | Fix #214. | Pierre Courtieu | |
| If this works we should probably change the generic function as well. | |||
| 2017-11-06 | Prettier cheat face (background + box). | Pierre Courtieu | |
| 2017-11-06 | Fix #135. | Pierre Courtieu | |
| 2017-10-26 | Limited extensibility of smie token detection. | Pierre Courtieu | |
| 2017-07-19 | changed -emacs-U flag to -emacs | Paul Steckler | |
| 2017-06-08 | Fixing a bug with Set/Unset commands due to recent commits. | Pierre Courtieu | |
| The "Show" inserted now and then would hide the result of Set/Unset commands. | |||
| 2017-06-06 | Adding a Set Silent + Show when backtracking into a proof. | Pierre Courtieu | |
| Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok. | |||
| 2017-05-25 | Merge pull request #185 from psteckler/remove-contribs | psteckler | |
| Remove mmm and ML4PG contribs | |||
| 2017-05-24 | Remove mmm and ML4PG contribs and remove references to them in code and docs | Paul Steckler | |
| 2017-05-23 | Fixing #183. | Pierre Courtieu | |
| 2017-05-16 | Fixing Set/Unset Printing broken by auto "Show". | Pierre Courtieu | |
| Current coq trunk has a bug with Show that I reported (there is a spurious Show executed) which makes C-u C-c C-a C-s fail for now. Should be fixed shortly. | |||
| 2017-05-12 | temporary fix of automatic intros. | Pierre Courtieu | |
| 2017-05-05 | Change (eval-when (compile) ...) to (eval-when-compile ...) | Clément Pit--Claudel | |
| This fixes a bunch of compilation warnings | |||
| 2017-05-05 | Merge pull request #157 from ProofGeneral/elpa | Clément Pit-Claudel | |
| [WIP] ELPA/MELPA support | |||
| 2017-04-25 | Typo from commit 758e679e. | Pierre Courtieu | |
| 2017-04-24 | Preparing new warning tags (no more special chars). | Pierre Courtieu | |
| 2017-04-19 | Fix #176. | Pierre Courtieu | |
| The code uses several token searcher and the wrong one was called somewhere. | |||
| 2017-03-31 | Fixing #173. | Pierre Courtieu | |
| 2017-03-22 | Added support for future new options (trunk). | Pierre Courtieu | |
| 2017-03-08 | Add a FIXME in coq.el | Clément Pit--Claudel | |
| 2017-03-08 | Remove uses of defpgdefault in coq-abbrev | Clément Pit--Claudel | |
| 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'. | |||
| 2017-03-08 | Remove uses of defpacustom in coq-compile-common | Clément Pit--Claudel | |
| 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!") | |||
| 2017-03-08 | Remove compile-time calls to proof-ready-for-assistant | Clément Pit--Claudel | |
| Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el. | |||
| 2017-03-08 | Remove unnecessary calls to 'eval-and-compile' | Clément Pit--Claudel | |
| 2017-03-08 | Fix incorrect uses of defvar | Clément Pit--Claudel | |
| 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. | |||
| 2017-03-08 | Fix incorrect assumption that noninteractive == byte-compiling | Clément Pit--Claudel | |
| The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. | |||
| 2017-03-08 | Merge commit '06fd76163b857a056ac44e7437efa17656f06e5b' | Paul Steckler | |
| 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-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-23 | Fixing #154. | Pierre Courtieu | |
| 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-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 | 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 #107 from JasonGross/patch-3 | hendriktews | |
| Add Context to coq-syntax.el | |||
| 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. | |||
| 2016-12-31 | add second argument to looking-back, required in emacs25 | 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-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 | fix :get for coq-search-blacklist | Hendrik Tews | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |