proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Fixed at-point detection.	Pierre Courtieu	2015-04-27
\|
*	bold unicode biders + Fixing highlighting in goals and response buffers + ↵	Pierre Courtieu	2015-04-14
\| \| \| \|	cleaning.
*	Debugging font-lock for ∀, ∃, and λ.	Pierre Courtieu	2015-04-13
\|
*	Added unicode forall in font-lock regexps.	Pierre Courtieu	2015-04-10
\|
*	Added comment.	Pierre Courtieu	2015-04-07
\|
*	Fixed coq-id definition to be correct wrt to coq grammar.	Pierre Courtieu	2015-04-07
\|
*	Fixed highlighting of evars.	Pierre Courtieu	2015-04-07
\|
*	Trying to prepare indentation cleaning...	Pierre Courtieu	2015-04-03
\|
*	Highlighting stuff in goals mode (C-c C-a C-h). Very basic for now.	Pierre Courtieu	2015-04-02
\|
*	Fix fill-paragraph merging comments and code (never fill code).	Pierre Courtieu	2015-04-01
\|
*	Fixed smie code for ";" + added \|\| in grammar.	Pierre Courtieu	2015-03-31
\| \| \| \| \|	Actually \|\| and + are overloaded and I don"t see how to deambiguate them. Indetation may be buggy until I found away.
*	Fixed a small bug in indentation.	Pierre Courtieu	2015-03-27
\|
*	Fix disable evar colorizing in coq file.	Pierre Courtieu	2015-03-27
\|
*	Fixed a regex for detecting ids at point.	Pierre Courtieu	2015-03-27
\|
*	Colorizing hyps names robustified. Still incomplete.	Pierre Courtieu	2015-03-26
\|
*	A command to set coq printing width smartly.	Pierre Courtieu	2015-03-26
\| \| \| \| \|	Set the width to the current goals window. Default binding: C-c C-a C-w.
*	A remark about project file in the documentation.	Pierre Courtieu	2015-03-26
\| \| \| \| \|	Saying that one -arg should be followed by only one option. For several options, put several -arg, ONE PER LINE.
*	Fixed a smal bug in colorizing response buffer.	Pierre Courtieu	2015-03-26
\| \| \| \| \| \|	First constructor of an inductive was colorized as a hyp name. Hyp name colorizing should be done another way. Using font-lock here is probably bad.
*	Fixed indetation of tryif then else.	Pierre Courtieu	2015-03-24
\|
*	fixed gfail hilighting.	Pierre Courtieu	2015-03-24
\|
*	added some keywords	Pierre Courtieu	2015-03-24
\|
*	Highlighting evars.	Pierre Courtieu	2015-03-23
\|
*	Fixed lazymatch and multimatch indentation/highlighting.	Pierre Courtieu	2015-03-23
\|
*	Some comments for future work.	Pierre Courtieu	2015-03-13
\|
*	Added a command to send Queries to coq, with completion (C-c C-a C-q).	Pierre Courtieu	2015-03-13
\| \| \| \| \|	Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag.
*	Customization variables for modules, section and proof indentation.	Pierre Courtieu	2015-03-05
\|
*	Fixed Proof end/start detection on Proof using ...	Pierre Courtieu	2015-03-04
\| \| \| \| \|	Was making scripting confused. P.
*	Fixed compilation issue with previous commit + CHANGE updates.	Pierre Courtieu	2015-03-04
\|
*	Mouse queries.	Pierre Courtieu	2015-03-03
\| \| \| \| \|	If enabled, allows to send queries to coq with (control/shift/control-shift) mouse-1.
*	Coqtop always restarted when switching script buffer.	Pierre Courtieu	2015-03-03
\| \| \| \| \| \|	This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options.
*	Making freeze buffer hace coq-response-more.	Pierre Courtieu	2015-02-24
\| \| \| \| \|	So that shortcuts work from this buffer. + colorizing.
*	Typo in last commit.	Pierre Courtieu	2015-02-23
\|
*	Fixed a bug in syntax table making fontlock and indentation fail.	Pierre Courtieu	2015-02-23
\| \| \| \|	After some command detecting things at point, the indentation was broken.
*	Fixed read-only error for compile before require option.	Pierre Courtieu	2015-02-11
\| \| \| \| \| \|	the emacs bug seems solved: the error with read-only always occur whatever locale is used. So I toggle read-only off in coq-compile-response.
*	replug removal of induction principle in SearAbout queries.	Pierre Courtieu	2015-02-09
\|
*	Adding function to grab things at point and send queries about it.	Pierre Courtieu	2015-02-09
\| \| \| \|	No shortcut yet but I am testing some "one click" stuff right now.
*	Removed a debugging message.	Pierre Courtieu	2015-02-06
\|
*	Fix colorization of for coq multiple hypothesis on the same line.	Pierre Courtieu	2015-02-05
\|
*	cleaned previous commits (generic variable to disable error coloring).	Pierre Courtieu	2015-02-04
\|
*	Fixed previous commit (wrong regexp).	Pierre Courtieu	2015-02-04
\|
*	coloring names in resposne and goals	Pierre Courtieu	2015-02-03
\|
*	beautified a bit error messages.	Pierre Courtieu	2015-02-03
\|
*	cleaning regexp.	Pierre Courtieu	2015-02-03
\|
*	Set double hit electric terminator back. Disabled by default.	Pierre Courtieu	2015-01-30
\|
*	Fix coq project parsing and interpreting for coq v8.5.	Pierre Courtieu	2015-01-27
\|
*	Fixed a bug in script navigation. Updated CHANGE	Pierre Courtieu	2015-01-27
\|
*	changed default indentation of match's cases.	Pierre Courtieu	2015-01-14
\|
*	failed and commented attempt at improving indentation of records.	Pierre Courtieu	2015-01-09
\|
*	Removing non-smie indentation + fix CHANGES.	Pierre Courtieu	2015-01-09
\|
*	Fixing indentation of pending curly braces.	Pierre Courtieu	2015-01-05
\|