diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9482bf92..52b73535 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: cases.ml 11708 2008-12-20 10:50:20Z msozeau $ *) open Util open Names @@ -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 *) |