ProofGeneral/PG

Issues

• Warnings with emacs 29.3

  #786 opened 3 months ago by fblanqui
  2

• PG gets confused by comment in _CoqProject file that involves "-arg"

  #794 opened 2 months ago by RalfJung
  1

• Incompatibility with `package-quickstart`

  #771 opened 6 months ago by monnier
  7

• PG does not position to error of vernacular commands

  #790 opened 3 months ago by hendriktews
  0

• File mode specification error: (void-variable coq-cmd-force-next-proof-kept)

  #775 opened 3 months ago by DaKnig
  15

• Indentation issue : "\in"

  #757 opened 8 months ago by KimayaBedarkar
  2

• Tons of warnings when using certain PG features

  #686 opened 2 years ago by RalfJung
  12

• bug: newlines misparsed as space in string litterals

  #773 opened 3 months ago by erikmd
  10

• PG does not position to error

  #781 opened 3 months ago by Matafou
  8

• REGRESSION: ProofGeneral cannot step over Fail correctly

  #779 opened 5 months ago by hendriktews
  10

• Why retracting before restarting coqtop?

  #770 opened 6 months ago by Matafou
  3

• Merging the Abella fork of PG

  #701 opened a year ago by phikal
  11

• Proof General gets into a state where it doesn't know what + is.

  #769 opened 6 months ago by walck
  11

• UI and kernel out of sync from aborting tactics?

  #764 opened 8 months ago by AndreasLoow
  1

• 3-pane mode broken with small frame heights

  #760 opened 8 months ago by hendriktews
  0

• different styles of comment

  #756 opened 8 months ago by ElifUskuplu
  6

• PG incorrectly interprets `}.` as a single token, which results in incorrectly accepting files that coqc rejects

  #690 opened 8 months ago by JasonGross
  3

• Automatic indenting for Easycrypt

  #702 opened a year ago by Adamw1NCSC
  1

• Bug: Frames in hybrid mode automatically revert to vertical mode

  #746 opened 9 months ago by allen-liaoo
  2

• test_wholefile.v incompatible with 8.19

  #719 opened a year ago by hendriktews
  4

• dynamic highlighting

  #738 opened 9 months ago by ElifUskuplu
  1

• Build failure when "Compile Before Require" meets imported OCaml plugins

  #724 opened 10 months ago by RalfJung
  13

• coq-load-project file should extract META files

  #736 opened 10 months ago by hendriktews
  1

• void function error

  #734 opened 10 months ago by ZHANGTIANYAO1
  0

• wait for proof-goto-point to finish

  #731 opened 10 months ago by aa755
  1

• proof-goto-point is non-idempotent

  #728 opened 10 months ago by aa755
  2

• "Omit proof" on a Let in a section leads to warning

  #687 opened a year ago by RalfJung
  14

• "Omit proofs" breaks other proofs because it also skips hints

  #688 opened a year ago by Blaisorblade
  14

• makeinfo reports warning: @inforef is obsolete

  #721 opened a year ago by hendriktews
  0

• generic/pg-goals.el shouldn't be executable

  #704 opened a year ago by SnarkBoojum
  1

• compile-tests/003-require-error fails sporadically with 8.19-rc1

  #722 opened a year ago by hendriktews
  4

• confusing error on incorrect _CoqProject file

  #707 opened a year ago by gasche
  0

• Compile-before-require setting does not presist

  #710 opened a year ago by vzaliva
  1

• `coq-insert-suggested-dependency` sometimes inserts unparsable statements

  #715 opened a year ago by HazardousPeach
  0

• Colors don't work in emacs-nox

  #709 opened a year ago by cryslith
  1

• test_wholefile.v incompatible with 8.17

  #698 opened 2 years ago by hendriktews
  1

• ProofGeneral does not handle "Proof term." directives

  #681 opened a year ago by RalfJung
  11

• Scheme ... with is indented improperly

  #700 opened 2 years ago by audreyseo
  1

• whitelist for admissible commands inside proofs

  #689 opened 2 years ago by hendriktews
  17

• Feature request: sparate commands for jumping to current point with/without omitting proofs

  #682 opened 2 years ago by RalfJung
  7

• *response* buffer only showing last output

  #684 opened 2 years ago by andremoeller
  3

• `coq-accept-proof-using-suggestion 'always` incorrectly believes that `proof` is a proof directive

  #674 opened 2 years ago by JasonGross
  4

• Broken link in Ch. 11 of User's Manual

  #678 opened 2 years ago by rebcabin
  0

• Interference with org-mode leads to buffer-save prompt of ephemeral buffers

  #668 opened 2 years ago by haselwarter
  4

• Hitting 'tab' to indent just throws an error

  #677 opened 2 years ago by RalfJung
  6

• Proof General overrides Emacs icon

  #672 opened 2 years ago by jeanas
  3

• Update https://proofgeneral.github.io/

  #673 opened 2 years ago by monnier
  2

• Feedback from Coq Community Survey 2022.

  #671 opened 2 years ago by Zimmi48
  1

• remove Isabelle walkthrough example

  #666 opened 2 years ago by HuStmpHrrr
  1

• Relative path in proof-autoloads doesn't seem to be relative

  #667 opened 2 years ago by ia0
  4