proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Fixed auto-width setting not initialized (trac #456).	Pierre Courtieu	2015-11-13
\|
*	Cleaning code for auto width adapting.	Pierre Courtieu	2015-11-13
\| \| \| \|	Less guessing, separate guessing code.
*	Tentative fix for #10	Clément Pit--Claudel	2015-11-12
\|
*	Close #9	Clément Pit--Claudel	2015-11-12
\|
*	Debuging: display a warning.	Pierre Courtieu	2015-11-12
\| \| \| \| \|	The warning is displayed when failing to retrieve last prompt info. Once we understand what happened we can remove this warning.
*	coq-pre-v85 option to fix coqdep invocation in [compile before require].	Pierre Courtieu	2015-11-02
\| \| \| \| \| \|	Command line options changed heavily betwenn 8.4 and 8.5. We need an option to force V8.4 in some cases, mainly to infer the right coqtop/coqdep invocations.
*	Re-thinking auto-insert-as.	Pierre Courtieu	2015-10-20
\| \| \| \| \| \| \| \| \|	Now there is acommand that adds as close to the next to be scripted command. Finally found a way to make this close to correct for destruct and induction by using "!" modifier on the destructed names, so that the automatic naming does not reuse the this name. Probably still very approximated for inversion.
*	Fixed the regexp for colorizing hyps in the goal.	Pierre Courtieu	2015-10-15
\|
*	Fixed coq-id-at-point.	Pierre Courtieu	2015-10-13
\|
*	proof-retract-command-hook added + more auto adjust width in coq mode.	Pierre Courtieu	2015-10-13
\|
*	proof-assert-command-hook added + Auto adjust width in coq mode.	Pierre Courtieu	2015-10-12
\| \| \| \| \| \| \|	This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing).
*	Trying to not delete frames too eagerly when laying out.	Pierre Courtieu	2015-10-09
\|
*	Fixing 4096 character limit of scomint-send-input.	Pierre Courtieu	2015-10-09
\| \| \| \| \|	Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24).
*	Fixing < 25 use of window-frame (mandatory arg).	Pierre Courtieu	2015-10-09
\|
*	Put 'delete-selection t on coq-terminator-insert	Clément Pit--Claudel	2015-10-06
\| \| \| \| \|	delete-selection-mode requires command that insert text to be annotated with a 'delete-selection property.
*	Move .cvsignore to .gitignore	Clément Pit--Claudel	2015-10-06
\|
*	Trying to deal with debug mode.	Pierre Courtieu	2015-10-06
\|
*	colorizing hypothesis in compact mode.	Pierre Courtieu	2015-09-29
\|
*	Fixed #1 (Missing space in coq-insert-intros).	Pierre Courtieu	2015-09-29
\| \| \| \|	Added a newline and removed the useless intros.
*	Cleaned TODO file in coq/.	Pierre Courtieu	2015-09-29
\|
*	More Fixes when issuing commands from another buffer.	Pierre Courtieu	2015-09-25
\|
*	Fixed bug when issuing commands from another buffer than scripting one.	Pierre Courtieu	2015-09-25
\| \| \| \| \|	Hooks modifying things in goals or response now try to operate on the right frame/windows.
*	hyps highlighting now supports compact contexts (in coq trunk soon).	Pierre Courtieu	2015-09-22
\|
*	Added a moderate support for double quotes in -arg lines of _CoqProject.	Pierre Courtieu	2015-06-23
\|
*	Update to CHANGE.	Pierre Courtieu	2015-06-23
\|
*	robustify last commit (disabling smie show-paren).	Pierre Courtieu	2015-05-19
\|
*	Disable smie parenthesis blink. Too slow sometimes.	Pierre Courtieu	2015-05-19
\|
*	Fixes #492. fixed regexp (\\< --> \\_< everywhere).	Pierre Courtieu	2015-05-07
\| \| \| \|	Surprising that this did not raise before...
*	Fixes #484. Added syntax.	Pierre Courtieu	2015-05-07
\|
*	Fixes #485.	Pierre Courtieu	2015-05-07
\|
*	Fixes #486 with an option.	Pierre Courtieu	2015-05-07
\|
*	Yet another half fix of smie lexer.	Pierre Courtieu	2015-05-07
\| \| \| \|	\|\| is either a boolean operator or a tactical.
*	Fixed at-point detection (bis).	Pierre Courtieu	2015-04-27
\|
*	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.