diff options
| author | Assia Mahboubi | 2008-01-31 16:04:19 +0000 |
|---|---|---|
| committer | Assia Mahboubi | 2008-01-31 16:04:19 +0000 |
| commit | 1dc8758152c89445de0c6db1d57e02e0942dea2b (patch) | |
| tree | 704118af726a71a74e41be3af8801daabf690fd1 /CHANGES | |
| parent | 5cf522a1e5c9231e64651e9cb95a1c4a45eed155 (diff) | |
updated CHANGES
added an example file in coq/
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -118,7 +118,7 @@ Default is now 8.1 (if no coqtop is found the path). These two functions allow to insert a tactic or command with completion in the mini-buffer. -*** New variables coq-user-commands-db and coq-user-tactics-db +*** New variables coq-user-commands-db, coq-user-keywords, coq-user-tactics-db User defined tactics/commands information. See C-h v coq-syntax-db for syntax. It is not necessary to add your own @@ -126,13 +126,17 @@ Default is now 8.1 (if no coqtop is found the path). synchronizing/backtracking system). You may however do so for the following reasons: - 1 your tactics/commands will be colorized by font-lock + 1 your tactics/commands/keyword will be colorized by font-lock 2 your tactics/commands will be added to the menu and to completion when calling coq-insert-tactic/command (see below) 3 you may define an abbreviation for your tactic/command. + The file coq/ex-ssreflect.v contains an example of such + customization, together with a coloured script containing + user-defined tactics/commands/keywords. + *** automatic insertion of "match...with" for a given type This coqide great feature has been added. |