summaryrefslogtreecommitdiff
path: root/src/GF/Grammar/Grammar.hs
diff options
context:
space:
mode:
authorkrasimir <krasimir@chalmers.se>2009-10-27 15:45:05 +0000
committerkrasimir <krasimir@chalmers.se>2009-10-27 15:45:05 +0000
commit83bc6d4cda927a9f2716958398da5d5684d96a8b (patch)
treed5d07f956509c89567ad6eaeb64b0355da0522cf /src/GF/Grammar/Grammar.hs
parent8ebb4e854a474ee376253b9d476a25c5d1f24e9b (diff)
simplify the Term again
Diffstat (limited to 'src/GF/Grammar/Grammar.hs')
-rw-r--r--src/GF/Grammar/Grammar.hs1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs
index 70153c454..1b76fe27e 100644
--- a/src/GF/Grammar/Grammar.hs
+++ b/src/GF/Grammar/Grammar.hs
@@ -131,7 +131,6 @@ data Term =
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
| R [Assign] -- ^ record: @{ p = a ; ...}@
| P Term Label -- ^ projection: @r.p@
- | PI Term Label Int -- ^ index-annotated projection
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
| Table Term Term -- ^ table type: @P => A@