index
:
proof-general
master
Emacs plugins for proof management systems
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
coq
/
ex
Age
Commit message (
Expand
)
Author
2020-10-16
Fix #514 + support for named goal selector.
Pierre Courtieu
2020-03-12
moving tests for monadic notations and Equations in separate files.
Pierre Courtieu
2020-03-12
Fix #465: Indentation of Equations (plugin).
Pierre Courtieu
2020-03-02
Adding Tests for indentation related to plugins.
Pierre Courtieu
2020-01-19
Generic monadic indentation + specifically ext-lib / Compcert + doc.
Pierre Courtieu
2019-06-17
fixing with inductive indentation.
Pierre Courtieu
2017-05-23
Fixing #183.
Pierre Courtieu
2017-03-03
Merge pull request #163 from ProofGeneral/fix_indentation
Pierre Courtieu
2017-03-02
use Utf8 from Coq library
Paul Steckler
2017-01-26
Fixing #147 and #91 + others indentation bugs.
Pierre Courtieu
2015-03-23
Fixed lazymatch and multimatch indentation/highlighting.
Pierre Courtieu
2015-01-05
Fixing indentation of pending curly braces.
Pierre Courtieu
2015-01-05
trying to indent pending forall in the expected way
Pierre Courtieu
2014-12-30
fixed indentation (lexing of 'with') + made local coq-load-path.
Pierre Courtieu
2014-12-24
fixed a bug in command parsing for coq, due to recent changes.
Pierre Courtieu
2014-06-06
* coq/coq-smie.el: Fix precedence of 'else'.
Stefan Monnier
2014-06-04
* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.
Stefan Monnier
2014-06-03
Rename coq-smie-lexer.el to coq-smie.el.
Stefan Monnier
2013-07-11
Fixing another bug in indentation concerning "where". Actually there
Pierre Courtieu
2012-11-13
- first version of parallel asynchronous compilation for coq in
Hendrik Tews
2012-07-10
Fixed incorrect syntax of previous commit.
Pierre Courtieu
2012-06-08
Indentation is a bit more accurate.
Pierre Courtieu
2012-06-07
Fix indentation of dependent match clauses (as ... in ... return ...).
Pierre Courtieu
2012-06-04
One more fix for indentation.
Pierre Courtieu
2012-06-03
Fix a bug of indentation.
Pierre Courtieu
2012-05-09
fix typo + add one missing cvsignore
Hendrik Tews
2012-02-10
Fixed an ineficiency in comment detection.
Pierre Courtieu
2011-12-27
Typo
David Aspinall
2011-07-08
Fixing the scripting of new subproof script parenthesizing ({ and }).
Pierre Courtieu
2011-07-01
Some more sample indentation patterns added.
Pierre Courtieu
2011-06-17
oops, undo last commit.
Pierre Courtieu
2011-06-10
Fix trac #410.
Pierre Courtieu
2011-06-08
Added one indentation example.
Pierre Courtieu
2011-06-04
Updated the old code for indentation, in case Stefan cannot finish the
Pierre Courtieu
2011-05-20
- minor changes: clean personal todo list + adjust test case description
Hendrik Tews
2011-05-12
- add test coq/ex/test-cases/change-ancestor for the
Hendrik Tews
2011-02-28
- adjust coq-ask-insert-coq-prog-name and doc in coq-local-vars-doc
Hendrik Tews
2011-01-26
- fix problem description
Hendrik Tews
2011-01-21
- use time-less-p
Hendrik Tews
2011-01-18
- fixed stale load path problem with killing the proof shell in
Hendrik Tews
2011-01-17
fix problems in test cases
Hendrik Tews
2011-01-14
- more coq test cases (some with surprising and embarrassing bugs)
Hendrik Tews
2011-01-14
- move proof-no-fully-processed-buffer to generic/proof-config
Hendrik Tews
2010-09-09
Fixed small bugs in indentation.
Pierre Courtieu
2010-09-08
illustrating the wrongness of the current multifile processing for coq.
Pierre Courtieu
2010-09-08
Added three files for testing multi file scripting.
Pierre Courtieu
2010-08-15
Moved files
David Aspinall
2010-08-13
Renamed file
David Aspinall