proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	fixed a bug in command parsing for coq, due to recent changes.	Pierre Courtieu	2014-12-24
\|
*	typo in indentation cod, found after testing coq/ex/indent.v.	Pierre Courtieu	2014-12-24
\|
*	fixing a small pb in indentation of arrow (->). Not perfect.	Pierre Courtieu	2014-12-24
\|
*	fixed the use of >= 24.4 function string-suffix-p.	Pierre Courtieu	2014-12-24
\|
*	Supporting more bullets (coq 8.5), like ++ or ++++.	Pierre Courtieu	2014-12-23
\|
*	Fix a special case in _CoqProject syntax (empty string).	Pierre Courtieu	2014-12-23
\|
*	Refix prettify compilation bug.	Pierre Courtieu	2014-12-23
\|
*	fixed comilation of prettify setting.	Pierre Courtieu	2014-12-23
\|
*	Fixed a compilation issue + small display glitch in coqpg	Pierre Courtieu	2014-12-22
\|
*	Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4.	Pierre Courtieu	2014-12-22
\|
*	Fixed response display spurious newlines for coq.	Pierre Courtieu	2014-12-18
\| \| \| \| \| \|	Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly.
*	Remove trailing space in info messages in coq mode.	Pierre Courtieu	2014-12-16
\|
*	Added a way to print eager message without warning face.	Pierre Courtieu	2014-12-16
\| \| \| \| \|	It is the only way I found to display informativemessage appearing before the goal.
*	make name filtering of searchabout more precise.	Pierre Courtieu	2014-12-09
\|
*	Added a variant of searchAbout hiding some spurious entries.	Pierre Courtieu	2014-12-09
\|
*	* coq/coq-smie.el: Fix precedence of 'else'.	Stefan Monnier	2014-06-06
\|
*	* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.	Stefan Monnier	2014-06-04
\| \| \| \| \|	(coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
*	Rename coq-smie-lexer.el to coq-smie.el.	Stefan Monnier	2014-06-03
\|
*	* coq.el (coq-prettify-symbols-alist): New var.	Stefan Monnier	2014-06-02
\| \| \| \|	(coq-mode-config): Use it.
*	Fixing coq project file parsing + moved project options.	Pierre Courtieu	2013-07-22
\|
*	fix type of coq-project-filename	Hendrik Tews	2013-07-17
\|
*	disable and protect coq-hide-additional-subgoals-switch for coq-time-commands	Hendrik Tews	2013-07-17
\|
*	add two Coq faq entries and improve some other	Hendrik Tews	2013-07-11
\|
*	fix typo and compilation	Hendrik Tews	2013-07-11
\|
*	fix two bugs in parallel compilation for Coq	Hendrik Tews	2013-07-11
\|
*	Fixing a big bug in coq project file management.	Pierre Courtieu	2013-07-11
\| \| \| \| \|	file and directory name were not adapted to where the current file is inside the directory structure. Now the absolute names are build.
*	Fixing another bug in indentation concerning "where". Actually there	Pierre Courtieu	2013-07-11
\| \| \| \| \|	are other uses of "where (declaring notation for records that I did no test).
*	Fixing #478 + reverting partially the fix of #476 (Instance cannot be ↵	Pierre Courtieu	2013-07-10
\| \| \| \|	indented by default).
*	Fixing #476 (bis). Adding Fixpoint as a goal starter.	Pierre Courtieu	2013-07-10
\|
*	Fixing #477. Adding Proposition as a goal-starter keyword.	Pierre Courtieu	2013-07-10
\|
*	Fixing #476. Adding more keywords for indentation like Lemma.	Pierre Courtieu	2013-07-10
\|
*	Fixing #475. the "=>" ptoken just before "exists" should be the ltac	Pierre Courtieu	2013-07-10
\| \| \| \|	"=>" most of the time.
*	Fixed interaction between file variables and coq project file + faq.	Pierre Courtieu	2013-07-09
\|
*	Updating coq/faq	Pierre Courtieu	2013-07-08
\|
*	Fixing again bug #466. With a bbetter solution.	Pierre Courtieu	2013-07-08
\| \| \| \|	Not using "b o f" token anymore.
*	Fixing #474. & is now an declared operator. I need something better to	Pierre Courtieu	2013-07-06
\| \| \| \|	capture any operator and give it a (configurable?) precedence.
*	Fixing #473. Now all token finishing by <symbol><dot> is considered an	Pierre Courtieu	2013-07-06
\| \| \| \|	end of command, except if exactly <dot><dot>
*	Fixing #466. Indent. bug when illformed commment at file beginning.	Pierre Courtieu	2013-07-05
\| \| \| \| \| \|	Nasty bug due to smie fallback to backward-sexp when finding an unknown token, namely the token "", which happens when reaching the bof. Had to add a specific token for b o f.
*	Fixing a compilation warning for a ml4pg function in coq.el.	Pierre Courtieu	2013-07-04
\|
*	Fixing undeclared variables for compilation.	Pierre Courtieu	2013-07-04
\|
*	Added faq for coq pg.	Pierre Courtieu	2013-07-02
\|
*	Fixing coq project file mechanism.	Pierre Courtieu	2013-07-02
\|
*	Adding support for coq project file for setting coqdoc args.	Pierre Courtieu	2013-06-19
\| \| \| \|	second attempt, seems better (cleaner code).
*	Adding support for coq project file for setting coqdoc args.	Pierre Courtieu	2013-06-19
\| \| \| \|	First attempt, seems ok.
*	Removing files from ML4PG folder	joheras	2013-05-31
\|
*	Removing ML4PG files from coq folder.	joheras	2013-05-31
\|
*	Removing ML4PG files from coq folder.	joheras	2013-05-31
\|
*	Inclusion of ML4PG in coq.el file.	joheras	2013-05-31
\|
*	* empty log message *	joheras	2013-05-31
\|
*	Removing hidden files of ML4PG.	joheras	2013-05-31
\|