diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-08 17:44:20 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-08 17:44:20 +0000 |
commit | c9467e5684f9a71cb82ddc72b5b9d501b32b5c5e (patch) | |
tree | a69b27a71cb8a846e2b0d48f960ed13d603b2446 /toplevel/locality.mli | |
parent | 8916db4378cf5ceb477a425bdf8f6bdd5fd58716 (diff) |
Protection against "Bad recursive type" in w_unify0 (bug #3036).
Morally, unification wants to unify "fun x:Meta => Meta"
with "fun x:nat => match x with ... end". Retyping is asked to
type "match x with ... end" in the context "x:Meta" where the
type of x has de facto been lost. Retyping fails.
I don't see an easy remedy since w_unify0 builds the unifier
lazily, and I'm not sure it is worth to propagate the unifier to
retyping so that it knows it. After all, the call to retyping in
w_unify0 is not so critical.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/locality.mli')
0 files changed, 0 insertions, 0 deletions