From 5cbc018fe934750bdf1043da68f99911be4ee6f6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 5 May 2015 19:25:24 +0200 Subject: Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for preserving compatibility of subst after #4214 being solved. --- CHANGES | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 87506dadc1..85a207c29f 100644 --- a/CHANGES +++ b/CHANGES @@ -5,6 +5,11 @@ Vernacular commands - New command "Redirect" to redirect the output of a command to a file. +Tactics + +- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where + it failed to substitute all substitutable equations or failed to simplify + cycles, or accidentally unfolded local definitions (flag is off by default). Changes from V8.5beta1 to V8.5beta2 =================================== @@ -19,7 +24,6 @@ Tactics - A script using the admit tactic can no longer be concluded by either Qed or Defined. In the first case, Admitted can be used instead. In the second case, a subproof should be used. - - The easy tactic and the now tactical now have a more predictable behavior, but they might now discharge some previously unsolved goals. @@ -27,25 +31,21 @@ Extraction - Definitions extracted to Haskell GHC should no longer randomly segfault when some Coq types cannot be represented by Haskell types. - - Definitions can now be extracted to Json for post-processing. Tools - Option -I -as has been removed, and option -R -as has been deprecated. In both cases, option -R can be used instead. - - coq_makefile now generates double-colon rules for rules such as clean. API - The interface of [change] has changed to take a [change_arg], which can be built from a [constr] using [make_change_arg]. - - [pattern_of_constr] now returns a triplet including the cleaned-up [evar_map], removing the evars that were turned into metas. - Changes from V8.4 to V8.5beta1 ============================== -- cgit v1.2.3 From d17090cee488844fddc444fdba4fd195c27707c7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 May 2015 17:32:38 +0200 Subject: Documenting the Loose Hint Behavior flag. --- CHANGES | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 85a207c29f..cb77c297dd 100644 --- a/CHANGES +++ b/CHANGES @@ -7,9 +7,18 @@ Vernacular commands Tactics -- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where +- New flag "Regular Subst Tactic" which fixes "subst" in situations where it failed to substitute all substitutable equations or failed to simplify cycles, or accidentally unfolded local definitions (flag is off by default). +- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a + special way. It accepts three distinct flags: + * "Lax", which is the default one, sets the old behavior, i.e. a non-imported + hint behaves the same as an imported one. + * "Warn" outputs a warning when a non-imported hint is used. Note that this is + an over-approximation, because a hint may be triggered by an eauto run that + will eventually fail and backtrack. + * "Strict" changes the behavior of an unloaded hint to the one of the fail + tactic, allowing to emulate the hopefully future import-scoped hint mechanism. Changes from V8.5beta1 to V8.5beta2 =================================== -- cgit v1.2.3 From 3a7095f9f6a09a4461c2124b0020dfe37962de26 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2015 17:47:24 +0200 Subject: Safer typing primitives. Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. --- CHANGES | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index cb77c297dd..080b460a86 100644 --- a/CHANGES +++ b/CHANGES @@ -20,6 +20,21 @@ Tactics * "Strict" changes the behavior of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. +API + +- Some functions from pretyping/typing.ml and their derivatives were potential + source of evarmap leaks, as they dropped their resulting evarmap. The + situation was clarified by renaming them according to a unsafe_* scheme. Their + sound variant is likewise renamed to their old name. The following renamings + were made. + * Typing.type_of -> unsafe_type_of + * Typing.e_type_of -> type_of + * A new e_type_of function that matches the e_ prefix policy + * Tacmach.pf_type_of -> pf_unsafe_type_of + * A new safe pf_type_of function. + All uses of unsafe_* functions should be eventually eliminated. + + Changes from V8.5beta1 to V8.5beta2 =================================== -- cgit v1.2.3 From 81eb133d64ac81cbf6962d624b20c1aa55c2baae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Apr 2015 11:16:05 +0200 Subject: Adding an option -w to control Coq warning output. For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings. --- CHANGES | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 080b460a86..d2890f7402 100644 --- a/CHANGES +++ b/CHANGES @@ -35,6 +35,10 @@ API All uses of unsafe_* functions should be eventually eliminated. +Tools + +- Added an option -w to control the output of coqtop warnings. + Changes from V8.5beta1 to V8.5beta2 =================================== -- cgit v1.2.3