diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /dev/doc/changes.txt | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'dev/doc/changes.txt')
-rw-r--r-- | dev/doc/changes.txt | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 069f7d42..322530e6 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,43 @@ ========================================= += CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = +========================================= + +** Functions in unification.ml have now the evar_map coming just after the env + +** Removal of Tacinterp.constr_of_id ** + +Use instead either global_reference or construct_reference in constrintern.ml. + +** Optimizing calls to Evd functions ** + +Evars are split into defined evars and undefined evars; for +efficiency, when an evar is known to be undefined, it is preferable to +use specific functions about undefined evars since these ones are +generally fewer than the defined ones. + +** Type changes in TACTIC EXTEND rules ** + +Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type +glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first +component is kept, the second one can be obtained via +Tacinterp.eval_tactic. + +** ARGUMENT EXTEND ** + +It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED +in ARGUMENT EXTEND statements. + +** Renaming of rawconstr to glob_constr ** + +The "rawconstr" type has been renamed to "glob_constr" for +consistency. The "raw" in everything related to former rawconstr has +been changed to "glob". For more details about the rationale and +scripts to migrate code using Coq's internals, see commits 13743, +13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December +2010) in Subversion repository. Contribs have been fixed too, and +commit messages there might also be helpful for migrating. + +========================================= = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= |