diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-30 04:25:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-30 04:27:35 +0100 |
| commit | 524f38b37fa744b7859d8c97bdec6bcbf27882aa (patch) | |
| tree | 1882fb4a1e118dadded9bdcd39abfdf04a93e53e /CHANGES | |
| parent | 9c4287c94700e19a70e0805d59cb4102a45326a7 (diff) | |
Documenting the Set Refine Instance Mode.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -63,6 +63,8 @@ Vernacular commands retrieved using the "Locate Term" command. - New "Derive" command to help writing program by derivation. - "Undo" undoes any command, not just tactics. +- New "Refine Instance Mode" option that allows to deactivate the generation of + obligations in incomplete typeclass instances, raising an error instead. Specification Language |