Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / ProofGeneral/PG issues and pull requests
#536 - make-temp-file without text argument for emacs 25
Pull Request -
State: closed - Opened by hendriktews over 3 years ago
- 1 comment
#532 - Compile tests
Pull Request -
State: closed - Opened by hendriktews almost 4 years ago
- 1 comment
#526 - fix coq-callcoq for emacs 27
Pull Request -
State: closed - Opened by hendriktews almost 4 years ago
- 1 comment
#503 - coq-par-compile: use hash for ancestors
Pull Request -
State: closed - Opened by hendriktews over 4 years ago
- 5 comments
Labels: kind: fix, part: coq-compile
#478 - coq-par-compile: support -vos for coq >= 8.11 and default setting change
Pull Request -
State: closed - Opened by hendriktews over 4 years ago
- 9 comments
#439 - Prooftree updates
Pull Request -
State: closed - Opened by hendriktews about 5 years ago
- 13 comments
#100 - coq-end-Section should handle Modules and Module Types
Issue -
State: open - Opened by tchajed about 8 years ago
#99 - Set Implicit Arguments is out of place in the options menu
Issue -
State: closed - Opened by tchajed about 8 years ago
- 3 comments
#98 - Ensure PG overlays have pg-span property
Pull Request -
State: closed - Opened by tchajed about 8 years ago
- 7 comments
#97 - Retracting to a point with multiple overlays fails
Issue -
State: closed - Opened by tchajed about 8 years ago
- 6 comments
#96 - coq-compile-before-require issue with Coq's command Add LoadPath
Issue -
State: open - Opened by jonleivent about 8 years ago
- 21 comments
#95 - Add Reserved Infix like Reserved Notation
Pull Request -
State: closed - Opened by JasonGross about 8 years ago
- 1 comment
#94 - some idtac output printed multiple times
Issue -
State: open - Opened by jonleivent about 8 years ago
- 1 comment
#93 - cannot use PG with trunk version of coq: Invalid version syntax: 'trunk'
Issue -
State: closed - Opened by jonleivent about 8 years ago
- 3 comments
#92 - Compile before require from current directory failing with 8.5
Issue -
State: closed - Opened by YaZko about 8 years ago
- 15 comments
#91 - Ltac redefs (::=) are not indented properly
Issue -
State: closed - Opened by jonleivent about 8 years ago
- 2 comments
#90 - idtac output is getting parsed by PG as commands
Issue -
State: closed - Opened by jonleivent about 8 years ago
- 5 comments
Labels: resolved: duplicate
#89 - PG not compiling with emacs 24.4
Issue -
State: closed - Opened by b1rd1e about 8 years ago
- 9 comments
#88 - Fix inforef references to the emacs manual.
Pull Request -
State: closed - Opened by yuvallanger about 8 years ago
- 1 comment
#87 - Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta)
Pull Request -
State: closed - Opened by erikmd about 8 years ago
- 1 comment
#86 - `proof-prog-name-ask` interacts poorly with tab-completion (especially on Windows)
Issue -
State: open - Opened by JasonGross about 8 years ago
- 4 comments
#85 - Highlight Existing Class like Existing Instance
Pull Request -
State: closed - Opened by JasonGross about 8 years ago
- 1 comment
#84 - Highlight [nra] like [nia] and [lia] and [lra]
Pull Request -
State: closed - Opened by JasonGross about 8 years ago
- 1 comment
#83 - Stuck with proof of software foundations.
Issue -
State: closed - Opened by mukeshtiwari about 8 years ago
- 9 comments
#82 - enhancement: easy way to colorize solution tactics that have some common regexp.
Issue -
State: closed - Opened by jonleivent about 8 years ago
- 4 comments
#81 - Existing Class is not completely colorized
Issue -
State: closed - Opened by jonleivent about 8 years ago
#80 - Strange indentation bug in Emacs master
Issue -
State: closed - Opened by cpitclaudel about 8 years ago
- 2 comments
#79 - coq-load-path docs: norec -> nonrec
Pull Request -
State: closed - Opened by tbrk over 8 years ago
- 8 comments
#78 - Color lia, romega, nia, psatz, nsatz, lra
Pull Request -
State: closed - Opened by JasonGross over 8 years ago
- 6 comments
#77 - `lia`, `romega`, `nia`, `psatz`, `nsatz`, `lra` should all be colored like `omega` and `reflexivity`
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 1 comment
#76 - Why do we call proof-locate-executable on coq-prog-name (et al)?
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 7 comments
#75 - Library more.v is required
Issue -
State: closed - Opened by YaZko over 8 years ago
- 7 comments
#74 - Free variable smie--parent
Issue -
State: open - Opened by psteckler over 8 years ago
- 3 comments
#73 - `Combined Scheme` should be highlighted
Issue -
State: open - Opened by JasonGross over 8 years ago
- 10 comments
#72 - `Include` should be highlighted
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 1 comment
#71 - Destructuring let breaks coq-Check et al.'s default suggestion
Issue -
State: closed - Opened by wilcoxjay over 8 years ago
- 13 comments
#70 - Coq trunk + compile before require => « Invalid version syntax: 'trunk' »
Issue -
State: closed - Opened by aspiwack over 8 years ago
- 12 comments
#69 - Coq compilation assumes that coqdep only returns .vo files
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 1 comment
#68 - Respect user settings in coq-insert-intros
Pull Request -
State: closed - Opened by cpitclaudel over 8 years ago
- 4 comments
#67 - intros! ignores some of ProofGeneral settings
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
#66 - ProofGenerar don't work with Isabelle2015 or higher
Issue -
State: closed - Opened by KeenS over 8 years ago
- 1 comment
#65 - proof-extend-queue: Wrong type argument: overlayp, nil
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 3 comments
#64 - Paragraph filling is no longer working
Issue -
State: closed - Opened by jwiegley over 8 years ago
- 6 comments
#63 - weird delay
Issue -
State: closed - Opened by lczch over 8 years ago
- 12 comments
Labels: resolved: wontfix
#62 - Time Command + bullets = PG hangs
Issue -
State: closed - Opened by jonleivent over 8 years ago
- 2 comments
#61 - PG does not compile
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 2 comments
#60 - change coq-prog-name from _CoqProject
Issue -
State: closed - Opened by SimonBoulier over 8 years ago
- 23 comments
#59 - Highlight ltac:(), constr:(), and uconstr:()
Pull Request -
State: closed - Opened by cpitclaudel over 8 years ago
- 1 comment
#58 - Statement splitting incorrect in the presence of some notation
Issue -
State: open - Opened by RalfJung over 8 years ago
- 9 comments
Labels: kind: enhancement, help wanted, resolved: wontfix
#57 - Errors encountered when a Compile Before Require fails
Issue -
State: closed - Opened by YaZko over 8 years ago
- 4 comments
Labels: resolved: duplicate
#56 - Proof General automatically resizes goals/response windows between proof steps
Issue -
State: closed - Opened by sdconsta over 8 years ago
- 15 comments
#55 - (Some) Imports from Coq standard library make the background compilation fail
Issue -
State: closed - Opened by RalfJung over 8 years ago
- 18 comments
#54 - Buffer coq-compile-response sometimes takes over the whole window
Issue -
State: open - Opened by RalfJung over 8 years ago
- 19 comments
Labels: resolved: duplicate
#53 - Electric terminator and newlines
Issue -
State: open - Opened by OndrejSlamecka over 8 years ago
- 5 comments
#52 - Edit Abbrevs broken?
Issue -
State: open - Opened by SimonBoulier over 8 years ago
- 2 comments
#51 - Support ssreflect-style indentation
Issue -
State: open - Opened by ejgallego over 8 years ago
- 10 comments
#50 - Implement support for "From ... Require ..."
Pull Request -
State: closed - Opened by RalfJung over 8 years ago
- 5 comments
#49 - Automatic compliation of dependencies does not work with Coq 8.5's "From ... Require Import..."
Issue -
State: closed - Opened by RalfJung over 8 years ago
- 4 comments
#48 - Update numbering flag passed to texi2html
Pull Request -
State: closed - Opened by tchajed over 8 years ago
#47 - lazymatch with bullets confuses C-M-f
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 3 comments
#46 - Failure while processing imports
Issue -
State: closed - Opened by YaZko over 8 years ago
- 7 comments
#45 - "Use project file" option does not work
Issue -
State: open - Opened by vzaliva over 8 years ago
- 4 comments
#44 - EasyCrypt PG mode
Pull Request -
State: closed - Opened by strub over 8 years ago
- 8 comments
Labels: kind: enhancement
#43 - easycrypt
Issue -
State: closed - Opened by spitters over 8 years ago
- 31 comments
Labels: kind: enhancement
#42 - Failed on-the-fly compilation dedicates goals window to compilation error message, confusing PG
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 5 comments
Labels: resolved: duplicate
#41 - query-replace inside the processed region selects the first match, rather than the next one
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 3 comments
#40 - basic proof tree changes for Coq 8.5
Pull Request -
State: closed - Opened by hendriktews over 8 years ago
- 4 comments
Labels: kind: enhancement
#39 - Undo does not revert the processed region
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 26 comments
#38 - More commands are not highlighted
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 8 comments
#37 - ProofGeneral incorrectly parses unterminated strings in comments in Coq
Issue -
State: open - Opened by JasonGross over 8 years ago
- 24 comments
#36 - Some commands are not highlighted correctly
Issue -
State: closed - Opened by JasonGross over 8 years ago
#35 - Do we support narrowing?
Issue -
State: open - Opened by cpitclaudel over 8 years ago
- 2 comments
#34 - ProofGeneral (sometimes?) does not build with Emacs 24.3.1 on Windows
Issue -
State: open - Opened by JasonGross over 8 years ago
- 2 comments
#33 - Cyclic dependencies
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 3 comments
#32 - warning building latest version d3d7622
Issue -
State: closed - Opened by jonleivent over 8 years ago
- 3 comments
#31 - Should we bind C-c C-j in terminals?
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 12 comments
#30 - prooftree is broken with 8.5 syntax
Issue -
State: closed - Opened by Matafou over 8 years ago
- 14 comments
#29 - Indentation is wrong after [exists]
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 4 comments
#28 - travis.yml for emacs 24.{3,4,5}
Pull Request -
State: closed - Opened by JasonGross over 8 years ago
- 1 comment
#27 - Add a .travis.yml file for continuous integration emacs 23, 24
Pull Request -
State: closed - Opened by JasonGross over 8 years ago
- 7 comments
#26 - Refactor the project file parsing code
Pull Request -
State: closed - Opened by cpitclaudel over 8 years ago
- 36 comments
#25 - PG gets confused when there is another frame visible at start
Issue -
State: closed - Opened by jonleivent over 8 years ago
- 2 comments
#24 - Tip of master is broken on Coq 8.4pl*
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 14 comments
#23 - Is there a way to make Double Hit Electric Terminator do an indent after the newline?
Issue -
State: closed - Opened by jonleivent over 8 years ago
- 3 comments
#22 - Fix spurious scrolling of *goals* and *response* buffers
Pull Request -
State: closed - Opened by cpitclaudel over 8 years ago
- 1 comment
#21 - Incompatibility in the handling of _CoqProject files between coq_makefile and ProofGeneral
Issue -
State: closed - Opened by JasonGross over 8 years ago
- 14 comments
#20 - Time Print foo doesn't print foo
Issue -
State: closed - Opened by jonleivent over 8 years ago
- 2 comments
#19 - Is `proof-shell-invisible-cmd-get-result' broken in Coq 8.5?
Issue -
State: closed - Opened by cpitclaudel over 8 years ago
- 4 comments
#18 - compile-before-require does not use _CoqProject options or Makefile
Issue -
State: closed - Opened by jonleivent almost 9 years ago
- 10 comments
#17 - "Setting" menu should we pre-fill string options for all provers
Issue -
State: open - Opened by Matafou almost 9 years ago
- 5 comments
#16 - cursor is covering up my code when used in the terminal
Issue -
State: closed - Opened by adnelson almost 9 years ago
- 2 comments
Labels: kind: question
#15 - indentation takes a long time, maybe forever
Issue -
State: closed - Opened by jonleivent almost 9 years ago
- 8 comments
#14 - How does one require proof-shell?
Issue -
State: closed - Opened by cpitclaudel almost 9 years ago
- 8 comments
#13 - 3 frames mode - get frames to appear at specific positions with specific sizes
Issue -
State: open - Opened by jonleivent almost 9 years ago
- 4 comments
#12 - Highlighting of evars
Issue -
State: closed - Opened by cpitclaudel almost 9 years ago
- 18 comments
#11 - We should edit the README
Issue -
State: closed - Opened by cpitclaudel almost 9 years ago
- 1 comment
#10 - constant msg: "Zero or more than one goals window, guessing window width."
Issue -
State: closed - Opened by jonleivent almost 9 years ago
- 24 comments
#9 - Add *.elc to .gitignore
Issue -
State: closed - Opened by jonleivent almost 9 years ago
- 1 comment
#8 - proofdepth sometimes ends up being nil
Issue -
State: open - Opened by cpitclaudel almost 9 years ago
- 2 comments
#7 - Request to add keystroke for Coq's "Print Assumptions" command
Issue -
State: closed - Opened by DavidAspinall almost 9 years ago
- 3 comments