aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* Coq indentation small fixes.Gravatar Pierre Courtieu2006-08-23
|
* fsf emacs compatibilty for symbol-at-point.Gravatar Pierre Courtieu2006-08-23
|
* Cleaning in coq and lib, fixed licenses and docstrings.Gravatar Pierre Courtieu2006-08-23
| | | | Added one or two details to docstring of generic variables.
* Finished making functions over big tables non recursive. Works withGravatar Pierre Courtieu2006-08-23
| | | | emacs.
* Making non recursive functions to make fsf emacs happy, not yet finished.Gravatar Pierre Courtieu2006-08-22
|
* Big redesign of the coq syntax defintion, centralization in big tablesGravatar Pierre Courtieu2006-08-22
| | | | like coq-commands-db.
* Menus redesign, new interactive tactics/commands/termsGravatar Pierre Courtieu2006-08-21
| | | | insertion. Great!
* Started the coq-insert-tactic.Gravatar Pierre Courtieu2006-08-21
|
* Moved the coq local variables tools in a separate file and made itGravatar Pierre Courtieu2006-08-17
| | | | simpler.
* continue on the support for local variables list semi-automaticGravatar Pierre Courtieu2006-08-17
| | | | | insertion. I put a new file in lib with basic tools for file variables lists.
* Added entries in coq menu, rearranged coq menu.Gravatar Pierre Courtieu2006-08-16
| | | | | Also added semi-automated setting of local file variables (*** Local Variables ***) coq-prog-name and coq-prog-args.
* fixed a bug with scripting with coq v8.0.Gravatar Pierre Courtieu2006-07-20
|
* removed debug messages from indentation code.Gravatar Pierre Courtieu2006-07-04
|
* fix the bug for coq indetation of two consecutive comments. Code isGravatar Pierre Courtieu2006-07-04
| | | | | ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is).
* fix a bug in coq indentation (loop). seems to be fixed. I still have aGravatar Pierre Courtieu2006-07-04
| | | | problem indenting comments (two consecutive comments: second shifted).
* moving coq-goal-command-p to indetation code, as from v8.1, goals areGravatar Pierre Courtieu2006-07-04
| | | | | | detected by the goal attribute of spans. syntactical goal recognizing is still used in indetation code, and for v8.0 compatibility. I shall remove v8.0 compatibility in some months.
* section backtracking bug fixed.Gravatar Pierre Courtieu2006-06-13
|
* Fix to work with coq 8.1 again (havent tested 8.0)Gravatar David Aspinall2006-05-26
|
* Remove debugsGravatar David Aspinall2006-05-26
|
* Changed the type of proof-goal-command-p. It takes now a span, whichGravatar Pierre Courtieu2006-04-26
| | | | | | allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
* made coq error regexp more preciseGravatar Pierre Courtieu2006-02-16
|
* CommentsGravatar David Aspinall2006-02-14
|
* Add example settings for coq-prog-args and coq-prog-envGravatar David Aspinall2006-02-14
|
* Cleanup version testing, prevent crash in case version string doesn't match.Gravatar David Aspinall2006-02-09
|
* typo in coq.el for regexp of sections.Gravatar Pierre Courtieu2006-01-28
|
* added some keyword to coq tacics.Gravatar Pierre Courtieu2005-11-28
|
* Added Module/EndGravatar David Aspinall2005-11-25
|
* Fix Pierre's emailGravatar David Aspinall2005-11-25
|
* Added holes to "math...with" generation from a type name.Gravatar Pierre Courtieu2005-11-09
|
* added match...with automatic building from atype name.Gravatar Pierre Courtieu2005-11-07
| | | | Had to correct a bug in proof-shell.
* Add more user preferences, fix existing ones.Gravatar David Aspinall2005-09-30
|
* Documentation.Gravatar David Aspinall2005-05-17
|
* added some entris in coq menus.Gravatar Pierre Courtieu2005-04-21
|
* cleaned a bit coq.el (checkdoc). Put some comments to tell what is toGravatar Pierre Courtieu2005-04-20
| | | | be removed when coq-8.0 becomes unsupported.
* New backtracking system for coq continues, this time it uses a new CoqGravatar Pierre Courtieu2005-04-20
| | | | | | | | | | | | | | | | | command "Bactrack n m p", where n is the global state label to reach backward, p is the number of aborts and m is an absolute reference to the proof stack to undo (it is the proof stack depth). Coq prompt is now like this: state proof stack num depth __ _ aux < 12 |aux|SmallStepAntiReflexive| 4 < ù ^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^ usual pending proofs usual special char See comments in coq-fin-and-forget-v81.
* small modifications, updating doc string of holes.el.Gravatar Pierre Courtieu2005-03-08
|
* making holes.el cleaner, with the help of Stefan Monnier. I had toGravatar Pierre Courtieu2005-03-08
| | | | adapt coq.el to these modifications.
* Updated the doc for new pg/coq. Made modifications advised by StefanGravatar Pierre Courtieu2005-02-17
| | | | Monnier on holes.el.
* Finished making holes.el a real minor-mode. There is a new fileGravatar Pierre Courtieu2005-02-15
| | | | | | | | | holes-load.el which defines the autoloads (enough of them?). All functions have the prefix "holes-", and offending keyboard shortcuts have been either removed or bound to the minor mode. I made holes-mode minor mode automatically turned on in all proof buffers in coq mode (including shell, script and response buffers as it may be useful to copy paste parts of this buffers into holes).
* cleaning holes.el. All functions are prefixed with "holes-". AlsoGravatar Pierre Courtieu2005-02-14
| | | | modified coq.el and coq-abbrev.el accordingly.
* Added simple testing framework (in progress)Gravatar David Aspinall2005-02-13
|
* Deleted compatibility for coq v6 and v7 + new backtracking system. ForGravatar Pierre Courtieu2005-02-10
| | | | now it can be triggered only by using coq-version-is-v8-1.
* Patch from Stefan Monnier:Gravatar David Aspinall2005-01-28
| | | | | | | | The * of (* is not quoted in the font-lock keywords leading to the possibility of matching the empty string, which tends to put font-lock in an infinite loop. Actually I think the infinite looping is due to a local bug in my experimental Emacs code, but the \\ is needed in order to really match what was intended.
* Add spaces after setting commands to separate. Temporarily disable ↵Gravatar David Aspinall2004-09-14
| | | | print-only-first-subgoal.
* debugged the indentation of coq (bug report of Batsiaan Zapf augustGravatar Pierre Courtieu2004-08-30
| | | | | 3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline).
* More proofgeneral.org removalsGravatar David Aspinall2004-08-25
|
* Fixed Coq version detection at start.Gravatar Pierre Courtieu2004-07-23
|
* adding the "Comments" keyword in state-preserving commands.Gravatar Pierre Courtieu2004-05-11
|
* Set comment-quote-nested (for Emacs/XEmacs 21.5)Gravatar David Aspinall2004-05-09
|
* added "User error" to error message (had already "User Error").Gravatar Pierre Courtieu2004-05-07
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 05:52:11 +0000