From b6dabf6aa5b96cfa3c11038316399f0797d734ac Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 25 Apr 2017 21:54:31 +0200 Subject: Refine test for unresolved evars: not reachable from initial evars The test is refined to handle aliases: i.e. undefined evars coming from restrictions and evar-evar unifications with an initial evar are not considered fresh unresolved evars. To check this, we generalize the restricted_evars set to an aliased_evars set in the evar map, registering evars being solved by another evar due to restriction or evar-evar unifications. This implements the proposal of PR #370 for testing the resolution status of evars independently of the evar-evar orientation order. This allows [apply] to refine an evar with a new one if it results from a [clear] request or an evar-evar solution only, otherwise the new evar is considered fresh and an error is raised. Also fixes bugs #4095 and #4413. Co-authored-by: Maxime Dénès --- .../02-specification-language/07825-rechable-from-evars.rst | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 doc/changelog/02-specification-language/07825-rechable-from-evars.rst (limited to 'doc') diff --git a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst new file mode 100644 index 0000000000..e57d5a7bc5 --- /dev/null +++ b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst @@ -0,0 +1,9 @@ +- **Changed:** + In :tacn:`refine`, new existential variables unified with existing ones are no + longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on + the orientation of evar-evar unification problems, and new existential variables + are always turned into (unshelved) goals. This can break compatibility in + some cases (`#7825 `_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 `_ and + `#4413 `_). -- cgit v1.2.3