diff options
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -24,6 +24,10 @@ Program - The "Shrink Obligations" flag now applies to all obligations, not only those solved by the automatic tactic. +Notations + +- "Bind Scope" can once again bind "Funclass" and "Sortclass". + Changes from V8.5beta3 to V8.5 ============================== @@ -103,9 +107,6 @@ solved by the automatic tactic. - Documented the Hint Cut command that allows control of the proof-search during typeclass resolution (see reference manual). -Notations -- "Bind Scope" can once again bind "Funclass" and "Sortclass". - API - Some functions from pretyping/typing.ml and their derivatives were potential |