diff options
| author | msozeau | 2008-11-27 17:54:05 +0000 |
|---|---|---|
| committer | msozeau | 2008-11-27 17:54:05 +0000 |
| commit | 066ba7e26f3c6849b9210e5ffee8d2d0c17c041d (patch) | |
| tree | a46a5e850878413b522d5e694677d759a4865eef | |
| parent | 8b61f54c09646dcc8284ee3269c88c35e0463c6b (diff) | |
Fix (?) a pattern matching compilation problem:
<<
Axiom A : nat -> bool.
Definition foo :=
match A 0 with
| true => true
| k => k
end.
Print foo.
>>
[A 0] is duplicated in the [k => k] branch!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11640 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3839561bf0..a4d0b25ce9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -150,8 +150,11 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) = then (* The body of pat is not needed to type j - see *) (* insert_aliases - and both deppat and nondeppat have the *) - (* same type, then one can freely substitute one by the other *) - subst1 nondeppat j.uj_val + (* same type, then one can freely substitute one by the other. *) + (* We use nondeppat only if it's a Rel to preserve sharing. *) + if isRel nondeppat then + subst1 nondeppat j.uj_val + else subst1 deppat j.uj_val else (* The body of pat is not needed to type j but its value *) (* is dependent in the type of j; our choice is to *) |