diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-12 13:18:42 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-17 23:38:26 +0200 |
commit | 741f3fab052b91eaec57f32b639ca722c3d8dc34 (patch) | |
tree | 3beff509deee6f7220017ca8d67eec3ee479210e /.mailmap | |
parent | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (diff) |
A fix for #5390 (a useful error on used introduction names was masked).
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.
We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.
Of course, the question of what best unification error to give in the
presence of backtracking is still open.
Diffstat (limited to '.mailmap')
0 files changed, 0 insertions, 0 deletions