proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Set version tag for new release.	David Aspinall	2011-06-09
\|
*	Fix compile errors (seems to be code duplication between coq.el and coq-indent)	David Aspinall	2011-06-09
\|
*	Update	David Aspinall	2011-06-09
\|
*	Add autoload.	David Aspinall	2011-06-09
\|
*	Added one indentation example.	Pierre Courtieu	2011-06-08
\|
*	- fix for #408: Only use the buffer name in	Hendrik Tews	2011-06-08
\| \| \| \| \|	coq-compile-response-buffer - fix typo elsewhere
*	2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca>	Stefan Monnier	2011-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \|	* coq/coq.el: Match Proof...Qed and fix ;-vs-\| precedence. (coq-smie-grammar): Add ; and \| tacticals. Rename decls => cmds. Add CoInductive, and Proof..Qed. (coq-smie-search-token-forward): Rename from coq-smie-search-token; make it more robust. (coq-smie-search-token-backward): New function. (coq-smie-forward-token, coq-smie-backward-token): Use it to distinguish Inductive's ":=" from other uses. (coq-smie-rules): Use smie-rule-separator for \|. Add ugly hack for Qed without matching "Proof".
*	Set version tag for new release.	David Aspinall	2011-06-07
\|
*	Summary: * coq.el (coq-smie-backward-token): Fix typo in last change.	Stefan Monnier	2011-06-07
\|
*	Summary: coq-smie: improve indentation.	Stefan Monnier	2011-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* coq.el (coq-smie-grammar): Add rules for {\|...\|}, Let, Record, Module..End, Section..End, and BeginSubproof..EndSubproof. (coq-smie-search-token): New function. (coq-smie-forward-token, coq-smie-backward-token): Recognize {\| and \|}. Distinguish Module definition from Module introduction. Merge "Module Type" and "Module". (coq-smie-rules): Refine list-intro. Improve indentation after "with". Add Function, Let and Record to the := case. Indent within Module..End and friends. Improve indentation of record def. Indent forall's body by 2. Better indent Lemmas. * coq-db.el (coq-build-abbrev-table-from-db): Mark those abbrevs as `system'. * coq-abbrev.el (coq-install-abbrevs): Don't bind save-abbrevs since it's not needed any more.
*	Summary: coq-smie: Do not assume all "." are terminators. Handle "Programs".	Stefan Monnier	2011-06-06
\| \| \| \| \| \|	(coq-smie-grammar): Add "Function" rule. (coq-smie-forward-token, coq-smie-backward-token): New functions. (coq-mode-config): Use them for the SMIE lexer.
*	Record of bug report sent	David Aspinall	2011-06-06
\|
*	* empty log message *	David Aspinall	2011-06-06
\|
*	Updated the old code for indentation, in case Stefan cannot finish the	Pierre Courtieu	2011-06-04
\| \| \| \| \| \| \|	new one for the release. Added also support for an experimental syntax modification: { .. } is a new syntax for Beginsubproof. ... EndSubproof. There a also few minor behavior changes. The code has changed a lot though.
*	Cleaning some keyboard shortcuts, applying patch from Erik Martin-Dorel.	Pierre Courtieu	2011-06-04
\|
*	coq-init-compile-response-buffer: handle killed buffer (Trac #408)	David Aspinall	2011-06-03
\|
*	proof-undo-and-delete-last-successful-command: obey spec (Trac #407)	David Aspinall	2011-06-03
\|
*	Set version tag for new release.	David Aspinall	2011-06-01
\|
*	Some small fixes in indentation for coq.	Pierre Courtieu	2011-05-31
\|
*	Added indentation for BeginSubProof/EndSubProof.	Pierre Courtieu	2011-05-31
\| \| \| \|	+ added some tactics syntax.
*	Set version tag for new release.	David Aspinall	2011-05-30
\|
*	Trac#403: wait for retraction to complete before returning, to	David Aspinall	2011-05-30
\| \| \| \|	avoid hitting read only error in calling command.
*	ensure (integerp proof-segment-up-to-cache-end), fixes Trac #404	David Aspinall	2011-05-27
\|
*	Set version tag for new release.	David Aspinall	2011-05-27
\|
*	proof-retract-before-change: fix Trac #403 (at least partially) by	David Aspinall	2011-05-26
\| \| \| \| \|	removing restriction during automatic retraction so proof-retract-until-point behaves correctly.
*	- two fixes for coq-debug-auto-compilation	Hendrik Tews	2011-05-25
\|
*	- minor changes: clean personal todo list + adjust test case description	Hendrik Tews	2011-05-20
\|
*	Fixed #394. There is a bug with kfont-lock-keywords. The workaround is	Pierre Courtieu	2011-05-17
\| \| \| \|	to change the order in which keywords appear. TO FIX.
*	Set version tag for new release.	David Aspinall	2011-05-16
\|
*	Update autogenerated files	David Aspinall	2011-05-16
\|
*	Update docstrings	David Aspinall	2011-05-16
\|
*	Patch for Trac#400.	David Aspinall	2011-05-16
\|
*	Ref to Coq chapter in PG manual	David Aspinall	2011-05-16
\|
*	Clean up customization groups for defpacustom and defpgcustom. See ↵	David Aspinall	2011-05-16
\| \| \| \|	http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000115.html.
*	Set version tag for new release.	David Aspinall	2011-05-12
\|
*	Update docstring magic	David Aspinall	2011-05-12
\|
*	Update autoloads	David Aspinall	2011-05-12
\|
*	Tweak for `proof-segment-up-to-using-cache': better handling of	David Aspinall	2011-05-12
\| \| \| \|	proof-last-edited-low-watermark.
*	Attempted fix for `proof-segment-up-to-using-cache', re	David Aspinall	2011-05-12
\| \| \| \|	http://proofgeneral.inf.ed.ac.uk/trac/ticket/395
*	- add test coq/ex/test-cases/change-ancestor for the	Hendrik Tews	2011-05-12
\| \| \| \|	change-ancestor bug
*	- add ".vo", ".glob" to completion-ignored-extensions when Proof	Hendrik Tews	2011-05-12
\| \| \| \|	General is loaded
*	Version year	David Aspinall	2011-05-06
\|
*	Checkdoc	David Aspinall	2011-05-06
\|
*	Fix emails	David Aspinall	2011-05-05
\|
*	Remove mention of dvi	David Aspinall	2011-05-05
\|
*	Set version tag for new release.	David Aspinall	2011-05-05
\|
*	Restore front page scary image. Update dates	David Aspinall	2011-05-05
\|
*	Update dates.	David Aspinall	2011-05-05
\|
*	Restore scary front page image. Add credits.	David Aspinall	2011-05-05
\|
*	Clean up and remove obsolete dvi targets.	David Aspinall	2011-05-05
\|