aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
authorletouzey2003-05-29 15:42:58 +0000
committerletouzey2003-05-29 15:42:58 +0000
commit5743ea67b5a615c419d349e891806828c0ddc549 (patch)
tree77b35fb934ae18ef04e2e2009914973527ef1e30 /kernel/typeops.ml
parent8fb775da36bd321428a0a6f9c73cc07dea6295f8 (diff)
:= dans un record engendre un LetIn qui n'etait pas géré
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions