index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
coq
Commit message (
Expand
)
Author
Age
*
Quick fix of a regression introduced by my last commit. Looking for a
Pierre Courtieu
2012-02-01
*
Fixed command end recognition in presence of operators of the form .+
Pierre Courtieu
2012-02-01
*
Fixed a small bug in indentation (ter repetita). Bullets are indented
Pierre Courtieu
2012-01-18
*
Fixed a small bug in indentation (bis repetita).
Pierre Courtieu
2012-01-18
*
Fixed a small bug in indentation.
Pierre Courtieu
2012-01-18
*
Support proof-shell-interactive-prompt-regexp, ref Trac #430
David Aspinall
2012-01-10
*
proof-shell-start-goals-regexp: shy match to avoid introducing match group
David Aspinall
2012-01-09
*
* fix case where some existential is instantiated with the last proof command
Hendrik Tews
2012-01-04
*
hide the dependent evars line
Hendrik Tews
2012-01-03
*
merge ProofTreeBranch into main trunk:
Hendrik Tews
2012-01-03
*
Extra test
David Aspinall
2011-12-27
*
Typo
David Aspinall
2011-12-27
*
Fixed some regexp. One for goal closing detection and one for
Pierre Courtieu
2011-12-16
*
Adapting coq syntax recognition to the future v8.4 behavior of bullets
Pierre Courtieu
2011-12-16
*
- protect proof-shell-handle-delayed-output against the case where
Hendrik Tews
2011-12-07
*
ensure optim-resp-window does not change the current buffer
Hendrik Tews
2011-12-06
*
Applied a patch from Tom Prince which makes
Pierre Courtieu
2011-12-05
*
Quick stab at support for switching to proof shell when interactive support e...
David Aspinall
2011-11-15
*
Small fixes to coq smie indentation.
Pierre Courtieu
2011-11-14
*
Fixed coq smie indentation.
Pierre Courtieu
2011-11-11
*
Fixed coq smie indentation.
Pierre Courtieu
2011-11-10
*
fixed some small bugs in coq indentation smie code.
Pierre Courtieu
2011-11-10
*
added utf8 quantifiers for indentation + small fix in indentation.
Pierre Courtieu
2011-11-08
*
Fixing syntax.
Pierre Courtieu
2011-11-07
*
Fixed a bit more smie coq indentation. Still unfinished but useable.
Pierre Courtieu
2011-11-07
*
Fixed several more bugs in smie indentation code. Not finished.
Pierre Courtieu
2011-11-05
*
slowly fixing the last small bugs in smie indentation.
Pierre Courtieu
2011-11-04
*
Fix previous commit (again).
Pierre Courtieu
2011-11-04
*
Fix previous commit.
Pierre Courtieu
2011-11-04
*
* coq.el (coq-smie-forward-token): Simplify by delegating to backward-token.
Stefan Monnier
2011-11-03
*
Fixed the indentation of different kinds of use of the with keyword.
Pierre Courtieu
2011-11-03
*
Added bullet indentation in smie code. smie code still needs some
Pierre Courtieu
2011-11-02
*
Attempt to support stricter bytecomp flags
David Aspinall
2011-10-17
*
Update dates and versions
David Aspinall
2011-10-03
*
Move a comment to docstring
David Aspinall
2011-10-03
*
fix coqdep warning treated as error (library occurring at
Hendrik Tews
2011-09-23
*
fix widget descriptions of coq-load-path
Hendrik Tews
2011-09-15
*
-add support for -R and -I -as in coq-load-path
Hendrik Tews
2011-09-15
*
fix #421 with solution 1
Hendrik Tews
2011-09-14
*
fix documentation error
Hendrik Tews
2011-09-09
*
Fix trac #420 indentation freezing.
Pierre Courtieu
2011-09-04
*
Non Unicode char
David Aspinall
2011-08-29
*
eval-when-compile -> eval-when (compile) to avoid defvar coq-prog-name
David Aspinall
2011-08-24
*
Add back annotation for docstring for texinfo
David Aspinall
2011-08-23
*
Note TODO for indent testing!
David Aspinall
2011-08-23
*
Move coq-prog-name back to coq.el
David Aspinall
2011-08-23
*
Crude patch for Trac #416. I haven't tried to understand indent code fully, ...
David Aspinall
2011-08-23
*
Fixing track 414 by adding Preterm as a state preserving command.
Pierre Courtieu
2011-07-29
*
Fix compile when smie isnt available
David Aspinall
2011-07-26
*
Fixing the scripting of new subproof script parenthesizing ({ and }).
Pierre Courtieu
2011-07-08
[next]