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
*
Updated.
David Aspinall
2004-04-14
*
added basic support for imenu for coq.
Pierre Courtieu
2004-04-14
*
added the "return" keyword to coq
Pierre Courtieu
2004-04-14
*
added some commands in coq menu
Pierre Courtieu
2004-04-06
*
fixed coq xsymb table.
Pierre Courtieu
2004-04-06
*
Fixed coq x-symbols. now alphaa is not encoded, aalpha is not encoded,
Pierre Courtieu
2004-04-05
*
Use official indentation\!
David Aspinall
2004-04-02
*
Remove three-buffer stuff (made generic)
David Aspinall
2004-04-02
*
changed ths syntax for sub/superscript:
Pierre Courtieu
2004-04-01
*
added subscript in x-symbols-coq.el.
Pierre Courtieu
2004-03-31
*
debugging coq-x-symbols.el
Pierre Courtieu
2004-03-30
*
added the forall x-symbol to the indent keywords lists.
Pierre Courtieu
2004-03-30
*
Trying to put x-symbols for coq. By copying
Pierre Courtieu
2004-03-30
*
*** empty log message ***
Pierre Courtieu
2004-03-29
*
V8/V7 reserved keywords for coq
Pierre Courtieu
2004-03-29
*
coq < 8.0 menu and abbrevs.
Pierre Courtieu
2004-03-19
*
adjusting to new syntax.
Pierre Courtieu
2004-03-18
*
coq menu twicking
Pierre Courtieu
2004-03-17
*
menu, holes and abbrev made better.
Pierre Courtieu
2004-03-17
*
Added 'Notation' stuff to coq menu command insert.
Pierre Courtieu
2004-03-16
*
added the abbreviation of Hint Rewrite.
Pierre Courtieu
2004-03-16
*
Added one entry in the coq insert command menu (hint rewrite).
Pierre Courtieu
2004-03-16
*
bug fix in holes (call to proof-indent-line instead of funcall
Pierre Courtieu
2004-03-15
*
little bug fix in coq-indent.el
Pierre Courtieu
2004-03-15
*
added proof-really-save-command-p to coq config, to deal with Proof
Pierre Courtieu
2004-03-11
*
bug fixes on indenting and command-end-regexp.
Pierre Courtieu
2004-03-11
*
fixed coq command-end expression-regexp to deal with the token '..'
Pierre Courtieu
2004-03-10
*
modification to avoid compile warnings (end)
Pierre Courtieu
2004-03-10
*
added a menu for hole operations
Pierre Courtieu
2004-03-10
*
compile warning corrections
Pierre Courtieu
2004-03-10
*
indentation for coq completely re-coded, because the generic mechanism
Pierre Courtieu
2004-03-08
*
Cleanup top-level forms (unused x binding)
David Aspinall
2004-03-01
*
setq-default -> defconst for module-kinds-table
David Aspinall
2004-03-01
*
Fix V7.4 -> V74
David Aspinall
2004-03-01
*
little changes of menu/holes/abbrev in coq/pg
Pierre Courtieu
2004-02-26
*
added menu entries to tactic menus
Pierre Courtieu
2004-02-19
*
added submenus for command insertion for coq. menu uses abbrev
Pierre Courtieu
2004-02-19
*
added some lines in holes short doc. And some abbrevs for coq.
Pierre Courtieu
2004-02-19
*
added some menu entries for coq.
Pierre Courtieu
2004-02-19
*
Coq Abbrevs now make holes. I will add a menu with basic command.
Pierre Courtieu
2004-02-18
*
Avoid type error if coq program can't be found during startup.
David Aspinall
2004-02-17
*
Added some interface stuff:
Pierre Courtieu
2004-02-11
*
little error in the syntax corrected.
Pierre Courtieu
2004-02-11
*
adapting to coq-8.0.
Pierre Courtieu
2004-02-06
*
Rever to simplest example
David Aspinall
2003-10-05
*
Make find-and-forget robust for proverproc regions
David Aspinall
2003-06-05
*
Fix some compile errors
David Aspinall
2003-02-24
*
corrected a bug of pg/coq, the following line was not recognized as a
Pierre Courtieu
2003-02-20
*
Added documentation string to the variables coq-version-is-V6 (new),
Pierre Courtieu
2003-02-16
*
Fixes so that compile works
David Aspinall
2003-02-15
[next]