proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Avoiding useless computation in indentation code.	Pierre Courtieu	2016-03-08
\|
*	Should fix #49 and #55 (compilation of From .. Require).	Pierre Courtieu	2016-03-08
\|
*	Small fix for -Q options in loadpath.	Pierre Courtieu	2016-03-08
\|
*	Highlight ltac:(), constr:(), and uconstr:()	Clément Pit--Claudel	2016-03-05
\| \| \| \|	Also refactor coq-font-lock-keywords-1 slightly.
*	Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)	Clément Pit--Claudel	2016-02-29
\|
*	Remove leftover comment	Clément Pit--Claudel	2016-02-28
\|
*	Don't add the ‘Time’ prefix to internal Coq commands	Clément Pit--Claudel	2016-02-28
\| \| \| \| \|	This ensures that parts of Proof General that use Coq commands in the background are not confused by extra timing information.
*	Add uconstr to the (ltac constr) list in SMIE	Clément Pit--Claudel	2016-02-27
\|
*	Fix a typo: s/coq-modulestart-proofstart/coq-indent-proofstart/	Clément Pit--Claudel	2016-02-27
\|
*	Add a :safe predicate to indentation variables	Clément Pit--Claudel	2016-02-27
\| \| \| \|	This is useful if people want to set them project-locally.
*	Simplify code to add to .emacs	Clément Pit--Claudel	2016-02-20
\|
*	Adding missing keywords	Pierre Courtieu	2016-02-18
\|
*	Merge pull request #28 from JasonGross/travis-24-3-4-5	Pierre Courtieu	2016-02-17
\|\ \| \| \| \|	travis.yml for emacs 24.{3,4,5}
* \	Merge pull request #40 from hendriktews/proof-tree	Pierre Courtieu	2016-02-17
\|\ \ \| \| \| \| \| \|	basic proof tree changes for Coq 8.5
* \| \|	More version number fixes	Clément Pit--Claudel	2016-02-13
\| \| \|
* \| \|	A few clarifications in README	Clément Pit--Claudel	2016-02-12
\| \| \|
* \| \|	Merge pull request #48 from tchajed/texi2html-flags	Clément Pit--Claudel	2016-02-10
\|\ \ \ \| \| \| \| \| \| \| \|	Update numbering flag passed to texi2html
\| * \| \|	Update numbering flag passed to texi2html	Tej Chajed	2016-02-10
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	texi2html, as of version 1.80 (http://download-mirror.savannah.gnu.org/releases//texi2html/NEWS-1.80), uses -number-sections instead of -number for the flag name.
* \| \|	More README updates	Clément Pit--Claudel	2016-02-10
\| \| \|
* \| \|	Update README	Clément Pit--Claudel	2016-02-10
\| \| \|
* \| \|	Ensure that version detection does not fail in 24.3	Clément Pit--Claudel	2016-02-06
\| \| \|
* \| \|	Use coq-prog-name to autodetect version number	Clément Pit--Claudel	2016-02-06
\| \| \|
* \| \|	Fixed recent coq syntax change (tac !H become tac (H)).	Pierre Courtieu	2016-01-27
\| \| \|
\| * \|	basic proof tree changes for Coq 8.5	Hendrik Tews	2016-01-24
\|/ / \| \| \| \| \| \| \| \| \| \|	Fixes to get basic proof tree functionality, including support for give_up, cycle, swap, revgoals. Unshelve and evar's don't work yet, see proof-tree issues #1 and #2
* \|	Cleaning CHANGES.	Pierre Courtieu	2016-01-19
\| \|
* \|	fix #36.	Pierre Courtieu	2016-01-19
\| \|
* \|	Add a few comments to explain values of coq-load-path	Clément Pit--Claudel	2016-01-14
\| \|
* \|	Mark coq-load-path-include-current as obsolete	Clément Pit--Claudel	2016-01-14
\| \|
* \|	Automatically detect which version of Coq we're using	Clément Pit--Claudel	2016-01-14
\| \|
* \|	Refactor the project file parsing code	Clément Pit--Claudel	2016-01-14
\| \|
* \|	Fix #29 + indentation glitch + regexp refactoring.	Pierre Courtieu	2016-01-14
\| \|
\| *	Versions 24.2 and earlier do not compile	Jason Gross	2016-01-13
\| \|
\| *	Add .travis.yml file adapted from fstar-mode.el	Jason Gross	2016-01-13
\|/ \| \| \|	From https://github.com/FStarLang/fstar-mode.el/blob/master/.travis.yml
*	Fixing indentation of ";".	Pierre Courtieu	2016-01-08
\| \| \| \| \|	Local/Global Tactic Notation
*	indentation of ";" more accurate.	Pierre Courtieu	2016-01-08
\| \| \| \| \|	Now detecting if the ; is inside a parenthesized tactic (--> no spurious indentation).
*	Fixing outdenting in ";" indetation.	Pierre Courtieu	2016-01-08
\|
*	Trying to indent ";" differently inside Ltac defs.	Pierre Courtieu	2016-01-08
\| \| \| \| \| \| \|	This only works when the command starts with "Ltac". Ideally we would like to switch to no indentation of ";" each time the ";" is the child of something else that ends a command "." or bullets).
*	Fixed indentation of ";" tactical.	Pierre Courtieu	2016-01-07
\|
*	Merge pull request #22 from ProofGeneral/fix-scrolling-buffers	Pierre Courtieu	2016-01-06
\|\ \| \| \| \|	Fix spurious scrolling of goals and response buffers
* \|	updating CHANGES	Pierre Courtieu	2016-01-06
\| \|
* \|	Adding uset preference coq-indent-semicolon-tactical.	Pierre Courtieu	2016-01-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some people prefer ";" tactical to be non indented, in particular in Ltac definitions. Setting this variable to 0 (2 by default) does it. You can still have some indentation by putting ; at beginning of lines: tac1 ; tac2 ; tac3.
* \|	Fixing #25.	Pierre Courtieu	2016-01-06
\| \| \| \| \| \| \| \|	proof-script-buffer was not set before calling proof-shell-ready-prover.
* \|	Fixing #20. #19 fixed by a commit in coq-8.5.	Pierre Courtieu	2016-01-06
\| \|
* \|	First try to fix #19 and #20. Not finished.	Pierre Courtieu	2016-01-04
\| \| \| \| \| \| \| \|	Maybe need coq fix.
\| *	Fix spurious scrolling of goals and response buffers	Clément Pit--Claudel	2015-12-31
\| \| \| \| \| \| \| \| \| \| \| \|	See https://github.com/cpitclaudel/company-coq/issues/8 and https://github.com/cpitclaudel/company-coq/issues/32 for some background info.
* \|	comment and readme.	Pierre Courtieu	2015-12-31
\| \|
* \|	Refactoring. New file coq-system.el.	Pierre Courtieu	2015-12-14
\|/
*	Small refactoring of coqxxx args detection.	Pierre Courtieu	2015-12-14
\| \| \| \| \| \|	Need some more refactoring actually: Some code from coq-compile-common became necessary to coq/pg globally. We shoudl refelct this by moving these parts somewhere else.
*	Fixing coq-prog-arg for auto compilation.	Pierre Courtieu	2015-12-14
\|
*	Fixing variable declaration.	Pierre Courtieu	2015-12-10
\|