proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
\|
*	Removing hidden files from ML4PG.	joheras	2013-05-31
\|
*	ML4PG modification	joheras	2013-05-31
\|
*	Documentation of ML4PG	joheras	2013-05-31
\|
*	ML4PG functionality added to Coq menu	joheras	2013-05-30
\|
*	* empty log message *	joheras	2013-05-30
\|
*	Adding some more standard utf8 symbols to indentation operator. We	Pierre Courtieu	2013-05-30
\| \| \| \|	really need some "operator" recognition here.
*	Fixing a minor bug in indetation (exists is tactic and a quantifier).	Pierre Courtieu	2013-05-29
\|
*	- update coq example	Hendrik Tews	2013-05-14
\| \| \| \|	- minor changes in user manual
*	improve doc	Hendrik Tews	2013-04-19
\|
*	fix overwriting the empty compilation queue	Hendrik Tews	2013-03-05
\|
*	small improvement	Hendrik Tews	2013-02-20
\|
*	fix parallel Coq compilation: report error for circular dependencies	Hendrik Tews	2013-02-18
\|
*	move message about killing coq compilation processes	Hendrik Tews	2013-02-18
\|
*	- implement retract from prooftree	Hendrik Tews	2013-01-20
\|
*	Fixed a bug with window height optimization.	Pierre Courtieu	2013-01-17
\| \| \| \| \|	When using unicode symbols, window-height (which is deprecated anyway) is incorrect, using window-text-height instead seems better.
*	- support Grab Existential Variables for Prooftree	Hendrik Tews	2013-01-17
\| \| \| \|	- protocol change, but stay at version 3
*	- support bullets and braces in Prooftree	Hendrik Tews	2013-01-15
\| \| \| \|	- prooftree protocol change to version 3
*	- fix asserting when parallel background compilation is in progress	Hendrik Tews	2013-01-03
\| \| \| \|	- fix aborting background compilation on error
*	- fix problem in emergency process killing	Hendrik Tews	2012-11-14
\| \| \| \|	- better handling of errors in process creation