diff options
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 = ========================================= |