diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly
index 5269747295..1540db4fa3 100644
--- a/spectec/src/frontend/parser.mly
+++ b/spectec/src/frontend/parser.mly
@@ -19,7 +19,8 @@ let positions_to_region position1 position2 =
 
 let at (l, r) = positions_to_region l r
 
-let ($$) it at = {it; at; note = ref ""}
+let ($) it pos = it $ at pos
+let ($$) it pos = it $$ at pos % ref ""
 
 
 (* Conversions *)
@@ -186,18 +187,18 @@ id : UPID { $1 } | LOID { $1 }
 id_lparen : UPID_LPAREN { $1 } | LOID_LPAREN { $1 }
 
 atomid_ : UPID { $1 }
-varid : LOID { $1 $ at $sloc }
-defid : id { $1 $ at $sloc } | IF { "if" $ at $sloc }
-relid : id { $1 $ at $sloc }
-gramid : id { $1 $ at $sloc }
+varid : LOID { $1 $ $sloc }
+defid : id { $1 $ $sloc } | IF { "if" $ $sloc }
+relid : id { $1 $ $sloc }
+gramid : id { $1 $ $sloc }
 hintid : id { $1 }
-fieldid : atomid_ { Atom $1 $$ at $sloc }
-dotid : DOTID { Atom $1 $$ at $sloc }
+fieldid : atomid_ { Atom $1 $$ $sloc }
+dotid : DOTID { Atom $1 $$ $sloc }
 
 atomid_lparen : UPID_LPAREN { $1 }
-varid_lparen : LOID_LPAREN { $1 $ at $sloc }
-defid_lparen : id_lparen { $1 $ at $sloc }
-gramid_lparen : id_lparen { $1 $ at $sloc }
+varid_lparen : LOID_LPAREN { $1 $ $sloc }
+defid_lparen : id_lparen { $1 $ $sloc }
+gramid_lparen : id_lparen { $1 $ $sloc }
 
 ruleid : ruleid_ { $1 }
 ruleid_ :
@@ -211,7 +212,7 @@ ruleid_ :
 atomid : atomid_ { $1 } | atomid DOTID { $1 ^ "." ^ $2 }
 
 atom :
-  | atom_ { $1 $$ at $sloc }
+  | atom_ { $1 $$ $sloc }
 atom_ :
   | atomid { Atom $1 }
   | TICK QUEST { Quest }
@@ -223,10 +224,10 @@ atom_ :
 
 varid_bind :
   | varid { $1 }
-  | atomid_ { Atom.make_var $1; $1 $ at $sloc }
+  | atomid_ { Atom.make_var $1; $1 $ $sloc }
 varid_bind_lparen :
   | varid_lparen { $1 }
-  | atomid_lparen { Atom.make_var $1; $1 $ at $sloc }
+  | atomid_lparen { Atom.make_var $1; $1 $ $sloc }
 
 enter_scope :
   | (* empty *) { Atom.enter_scope () }
@@ -234,7 +235,7 @@ exit_scope :
   | (* empty *) { Atom.exit_scope () }
 
 check_atom :
-  | UPID EOF { Atom.is_var (El.Convert.strip_var_suffix ($1 $ at $sloc)).it }
+  | UPID EOF { Atom.is_var (El.Convert.strip_var_suffix ($1 $ $sloc)).it }
 
 
 (* Operators *)
@@ -265,7 +266,7 @@ check_atom :
   | DARROW2 { EquivOp }
 
 %inline infixop :
-  | infixop_ { $1 $$ at $sloc }
+  | infixop_ { $1 $$ $sloc }
 %inline infixop_ :
   | DOT { Dot }
   | DOTDOT { Dot2 }
@@ -275,7 +276,7 @@ check_atom :
   | ARROW { Arrow }
 
 %inline relop :
-  | relop_ { $1 $$ at $sloc }
+  | relop_ { $1 $$ $sloc }
 %inline relop_ :
   | COLON { Colon }
   | SUB { Sub }
@@ -308,7 +309,7 @@ iter :
 
 (* Types *)
 
-typ_prim : typ_prim_ { $1 $ at $sloc }
+typ_prim : typ_prim_ { $1 $ $sloc }
 typ_prim_ :
   | varid { VarT ($1, []) }
   | varid_lparen comma_list(arg) RPAREN { VarT ($1, $2) }
@@ -319,7 +320,7 @@ typ_prim_ :
   | REAL { NumT RealT }
   | TEXT { TextT }
 
-typ_post : typ_post_ { $1 $ at $sloc }
+typ_post : typ_post_ { $1 $ $sloc }
 typ_post_ :
   | typ_prim_ { $1 }
   | LPAREN tup_list(typ) RPAREN
@@ -328,7 +329,7 @@ typ_post_ :
 
 typ : typ_post { $1 }
 
-deftyp : deftyp_ { $1 $ at $sloc }
+deftyp : deftyp_ { $1 $ $sloc }
 deftyp_ :
   | nottyp { $1.it }
   | LBRACE comma_nl_list(fieldtyp) RBRACE { StrT $2 }
@@ -357,48 +358,48 @@ deftyp_ :
   | nl_bar_list1(enumtyp(enum1), enumtyp(arith)) { RangeT $1 }
 
 
-(*nottyp_prim : nottyp_prim_ { $1 $ at $sloc }*)
+(*nottyp_prim : nottyp_prim_ { $1 $ $sloc }*)
 nottyp_prim_ :
   | typ_prim { $1.it }
   | atom { AtomT $1 }
   | atomid_lparen nottyp RPAREN
     { SeqT [
-        AtomT (Atom $1 $$ at $loc($1)) $ at $loc($1);
-        ParenT $2 $ at $loc($2)
+        AtomT (Atom $1 $$ $loc($1)) $ $loc($1);
+        ParenT $2 $ $loc($2)
       ] }
   | TICK LPAREN nottyp RPAREN
-    { BrackT (LParen $$ at $loc($2), $3, RParen $$ at $loc($4)) }
+    { BrackT (LParen $$ $loc($2), $3, RParen $$ $loc($4)) }
   | TICK LBRACK nottyp RBRACK
-    { BrackT (LBrack $$ at $loc($2), $3, RBrack $$ at $loc($4)) }
+    { BrackT (LBrack $$ $loc($2), $3, RBrack $$ $loc($4)) }
   | TICK LBRACE nottyp RBRACE
-    { BrackT (LBrace $$ at $loc($2), $3, RBrace $$ at $loc($4)) }
+    { BrackT (LBrace $$ $loc($2), $3, RBrace $$ $loc($4)) }
   | LPAREN tup_list(nottyp) RPAREN
     { match $2 with [t], false -> ParenT t | ts, _ -> TupT ts }
 
-nottyp_post : nottyp_post_ { $1 $ at $sloc }
+nottyp_post : nottyp_post_ { $1 $ $sloc }
 nottyp_post_ :
   | nottyp_prim_ { $1 }
   | nottyp_post iter { IterT ($1, $2) }
 
-nottyp_seq : nottyp_seq_ { $1 $ at $sloc }
+nottyp_seq : nottyp_seq_ { $1 $ $sloc }
 nottyp_seq_ :
   | nottyp_post_ { $1 }
   | nottyp_post nottyp_seq { SeqT ($1 :: as_seq_typ $2) }
 
-nottyp_un : nottyp_un_ { $1 $ at $sloc }
+nottyp_un : nottyp_un_ { $1 $ $sloc }
 nottyp_un_ :
   | nottyp_seq_ { $1 }
-  | infixop nottyp_un { InfixT (SeqT [] $ at $loc($1), $1, $2) }
+  | infixop nottyp_un { InfixT (SeqT [] $ $loc($1), $1, $2) }
 
-nottyp_bin : nottyp_bin_ { $1 $ at $sloc }
+nottyp_bin : nottyp_bin_ { $1 $ $sloc }
 nottyp_bin_ :
   | nottyp_un_ { $1 }
   | nottyp_bin infixop nottyp_bin { InfixT ($1, $2, $3) }
 
-nottyp_rel : nottyp_rel_ { $1 $ at $sloc }
+nottyp_rel : nottyp_rel_ { $1 $ $sloc }
 nottyp_rel_ :
   | nottyp_bin_ { $1 }
-  | relop nottyp_rel { InfixT (SeqT [] $ at $loc($1), $1, $2) }
+  | relop nottyp_rel { InfixT (SeqT [] $ $loc($1), $1, $2) }
   | nottyp_rel relop nottyp_rel { InfixT ($1, $2, $3) }
 
 nottyp : nottyp_rel { $1 }
@@ -415,14 +416,14 @@ casetyp :
 
 %inline enum1 :
   | exp_lit { $1 }
-  | PLUS arith_un { UnE (PlusOp, $2) $ at $sloc }
-  | MINUS arith_un { UnE (MinusOp, $2) $ at $sloc }
+  | PLUS arith_un { UnE (PlusOp, $2) $ $sloc }
+  | MINUS arith_un { UnE (MinusOp, $2) $ $sloc }
   | DOLLAR LPAREN exp RPAREN { $3 }
 
 
 (* Expressions *)
 
-exp_lit : exp_lit_ { $1 $ at $sloc }
+exp_lit : exp_lit_ { $1 $ $sloc }
 exp_lit_ :
   | BOOLLIT { BoolE $1 }
   | NATLIT { NatE (DecOp, $1) }
@@ -433,12 +434,12 @@ exp_lit_ :
 exp_var_ :
   | varid { VarE ($1, []) }
   | varid_lparen comma_list(arg) RPAREN { VarE ($1, $2) }
-  | BOOL { VarE ("bool" $ at $sloc, []) }
-  | NAT { VarE ("nat" $ at $sloc, []) }
-  | INT { VarE ("int" $ at $sloc, []) }
-  | RAT { VarE ("rat" $ at $sloc, []) }
-  | REAL { VarE ("real" $ at $sloc, []) }
-  | TEXT { VarE ("text" $ at $sloc, []) }
+  | BOOL { VarE ("bool" $ $sloc, []) }
+  | NAT { VarE ("nat" $ $sloc, []) }
+  | INT { VarE ("int" $ $sloc, []) }
+  | RAT { VarE ("rat" $ $sloc, []) }
+  | REAL { VarE ("real" $ $sloc, []) }
+  | TEXT { VarE ("text" $ $sloc, []) }
 
 exp_call_ :
   | DOLLAR defid { CallE ($2, []) }
@@ -452,7 +453,7 @@ exp_hole_ :
   | SKIP { HoleE (`Skip, `Next) }
   | MULTISKIP { HoleE (`Skip, `Rest) }
 
-(*exp_prim : exp_prim_ { $1 $ at $sloc }*)
+(*exp_prim : exp_prim_ { $1 $ $sloc }*)
 exp_prim_ :
   | exp_lit_ { $1 }
   | exp_var_ { $1 }
@@ -463,14 +464,14 @@ exp_prim_ :
   | LPAREN tup_list(exp_bin) RPAREN
     { match $2 with [e], false -> ParenE (e, false) | es, _ -> TupE es }
   | TICK LPAREN exp RPAREN
-    { BrackE (LParen $$ at $loc($2), $3, RParen $$ at $loc($4)) }
+    { BrackE (LParen $$ $loc($2), $3, RParen $$ $loc($4)) }
   | TICK LBRACK exp RBRACK
-    { BrackE (LBrack $$ at $loc($2), $3, RBrack $$ at $loc($4)) }
+    { BrackE (LBrack $$ $loc($2), $3, RBrack $$ $loc($4)) }
   | TICK LBRACE exp RBRACE
-    { BrackE (LBrace $$ at $loc($2), $3, RBrace $$ at $loc($4)) }
+    { BrackE (LBrace $$ $loc($2), $3, RBrace $$ $loc($4)) }
   | DOLLAR LPAREN arith RPAREN { $3.it }
 
-exp_post : exp_post_ { $1 $ at $sloc }
+exp_post : exp_post_ { $1 $ $sloc }
 exp_post_ :
   | exp_prim_ { signify_pars Post $1 }
   | exp_atom LBRACK arith RBRACK { IdxE ($1, $3) }
@@ -480,31 +481,31 @@ exp_post_ :
   | exp_atom iter { IterE ($1, $2) }
   | exp_post dotid { DotE ($1, $2) }
 
-exp_atom : exp_atom_ { $1 $ at $sloc }
+exp_atom : exp_atom_ { $1 $ $sloc }
 exp_atom_ :
   | exp_post_ { $1 }
   | atom { AtomE $1 }
   | atomid_lparen exp RPAREN
     { SeqE [
-        AtomE (Atom $1 $$ at $loc($1)) $ at $loc($1);
-        ParenE ($2, false) $ at $loc($2)
+        AtomE (Atom $1 $$ $loc($1)) $ $loc($1);
+        ParenE ($2, false) $ $loc($2)
       ] }
 
-exp_seq : exp_seq_ { $1 $ at $sloc }
+exp_seq : exp_seq_ { $1 $ $sloc }
 exp_seq_ :
   | exp_atom_ { signify_pars Seq $1 }
   | exp_seq exp_atom { SeqE (as_seq_exp $1 @ [$2]) }
   | exp_seq FUSE exp_atom { FuseE ($1, $3) }
 
-exp_un : exp_un_ { $1 $ at $sloc }
+exp_un : exp_un_ { $1 $ $sloc }
 exp_un_ :
   | exp_seq_ { signify_pars Op $1 }
   | bar exp bar { LenE $2 }
   | BARBAR gramid BARBAR { SizeE $2 }
   | NOT exp_un { UnE (NotOp, $2) }
-  | infixop exp_un { InfixE (SeqE [] $ at $loc($1), $1, $2) }
+  | infixop exp_un { InfixE (SeqE [] $ $loc($1), $1, $2) }
 
-exp_bin : exp_bin_ { $1 $ at $sloc }
+exp_bin : exp_bin_ { $1 $ $sloc }
 exp_bin_ :
   | exp_un_ { $1 }
   | exp_bin COMPOSE exp_bin { CompE ($1, $3) }
@@ -512,11 +513,11 @@ exp_bin_ :
   | exp_bin cmpop exp_bin { CmpE ($1, $2, $3) }
   | exp_bin boolop exp_bin { BinE ($1, $2, $3) }
 
-exp_rel : exp_rel_ { $1 $ at $sloc }
+exp_rel : exp_rel_ { $1 $ $sloc }
 exp_rel_ :
   | exp_bin_ { $1 }
-  | comma exp_rel { CommaE (SeqE [] $ at $loc($1), $2) }
-  | relop exp_rel { InfixE (SeqE [] $ at $loc($1), $1, $2) }
+  | comma exp_rel { CommaE (SeqE [] $ $loc($1), $2) }
+  | relop exp_rel { InfixE (SeqE [] $ $loc($1), $1, $2) }
   | exp_rel comma exp_rel { CommaE ($1, $3) }
   | exp_rel relop exp_rel { InfixE ($1, $2, $3) }
 
@@ -524,10 +525,10 @@ exp : exp_rel { $1 }
 
 fieldexp :
   | fieldid exp_post+
-    { ($1, match $2 with [e] -> e | es -> SeqE es $ at $loc($2)) }
+    { ($1, match $2 with [e] -> e | es -> SeqE es $ $loc($2)) }
 
 
-arith_prim : arith_prim_ { $1 $ at $sloc }
+arith_prim : arith_prim_ { $1 $ $sloc }
 arith_prim_ :
   | exp_lit_ { $1 }
   | exp_var_ { $1 }
@@ -551,25 +552,25 @@ arith_prim_ :
       IterE ($2, Opt) }
   | DOLLAR LPAREN exp RPAREN { $3.it }
 
-arith_post : arith_post_ { $1 $ at $sloc }
+arith_post : arith_post_ { $1 $ $sloc }
 arith_post_ :
   | arith_prim_ { $1 }
   | arith_atom UP arith_prim { BinE ($1, ExpOp, $3) }
   | arith_atom LBRACK arith RBRACK { IdxE ($1, $3) }
   | arith_post dotid { DotE ($1, $2) }
 
-arith_atom : arith_atom_ { $1 $ at $sloc }
+arith_atom : arith_atom_ { $1 $ $sloc }
 arith_atom_ :
   | arith_post_ { $1 }
   | atom { AtomE $1 }
 
-arith_un : arith_un_ { $1 $ at $sloc }
+arith_un : arith_un_ { $1 $ $sloc }
 arith_un_ :
   | arith_atom_ { $1 }
   | bar exp bar { LenE $2 }
   | unop arith_un { UnE ($1, $2) }
 
-arith_bin : arith_bin_ { $1 $ at $sloc }
+arith_bin : arith_bin_ { $1 $ $sloc }
 arith_bin_ :
   | arith_un_ { $1 }
   | arith_bin binop arith_bin { BinE ($1, $2, $3) }
@@ -579,7 +580,7 @@ arith_bin_ :
 arith : arith_bin { $1 }
 
 
-path : path_ { $1 $ at $sloc }
+path : path_ { $1 $ $sloc }
 path_ :
   | (* empty *) { RootP }
   | path LBRACK arith RBRACK { IdxP ($1, $3) }
@@ -595,41 +596,41 @@ premise_list :
 premise_bin_list :
   | nl_dash_list(premise_bin) { $1 }
 
-(*premise_post : premise_post_ { $1 $ at $sloc }*)
+(*premise_post : premise_post_ { $1 $ $sloc }*)
 premise_post_ :
   | OTHERWISE { ElsePr }
   | LPAREN premise RPAREN iter*
     { let rec iters prem = function
         | [] -> prem
-        | iter::iters' -> iters (IterPr (prem, iter) $ at $sloc) iters'
+        | iter::iters' -> iters (IterPr (prem, iter) $ $sloc) iters'
       in (iters $2 $4).it }
 
-premise_bin : premise_bin_ { $1 $ at $sloc }
+premise_bin : premise_bin_ { $1 $ $sloc }
 premise_bin_ :
   | premise_post_ { $1 }
   | relid COLON exp_bin { RulePr ($1, $3) }
   | IF exp_bin
     { let rec iters e =
         match e.it with
-        | IterE (e1, iter) -> IterPr (iters e1 $ e1.at, iter)
+        | IterE (e1, iter) -> IterPr (Source.(iters e1 $ e1.at), iter)
         | _ -> IfPr e
       in iters $2 }
 
-premise : premise_ { $1 $ at $sloc }
+premise : premise_ { $1 $ $sloc }
 premise_ :
   | premise_post_ { $1 }
   | relid COLON exp { RulePr ($1, $3) }
   | IF exp
     { let rec iters e =
         match e.it with
-        | IterE (e1, iter) -> IterPr (iters e1 $ e1.at, iter)
+        | IterE (e1, iter) -> IterPr (Source.(iters e1 $ e1.at), iter)
         | _ -> IfPr e
       in iters $2 }
 
 
 (* Grammars *)
 
-(*sym_prim : sym_prim_ { $1 $ at $sloc }*)
+(*sym_prim : sym_prim_ { $1 $ $sloc }*)
 sym_prim_ :
   | gramid { VarG ($1, []) }
   | gramid_lparen comma_list(arg) RPAREN { VarG ($1, $2) }
@@ -642,23 +643,23 @@ sym_prim_ :
     { match $2 with [g], false -> ParenG g | gs, _ -> TupG gs }
   | DOLLAR LPAREN arith RPAREN { ArithG $3 }
 
-sym_post : sym_post_ { $1 $ at $sloc }
+sym_post : sym_post_ { $1 $ $sloc }
 sym_post_ :
   | sym_prim_ { $1 }
   | sym_post iter { IterG ($1, $2) }
 
-sym_attr : sym_attr_ { $1 $ at $sloc }
+sym_attr : sym_attr_ { $1 $ $sloc }
 sym_attr_ :
   | sym_post_ { $1 }
   | sym_post COLON sym_post { AttrG (El.Convert.exp_of_sym $1, $3) }
 
-sym_seq : sym_seq_ { $1 $ at $sloc }
+sym_seq : sym_seq_ { $1 $ $sloc }
 sym_seq_ :
   | sym_attr_ { $1 }
   | sym_seq sym_attr { SeqG (as_seq_sym $1 @ [Elem $2]) }
   | sym_seq NL_NL_NL sym_attr { SeqG (as_seq_sym $1 @ [Nl; Elem $3]) }
 
-sym_alt : sym_alt_ { $1 $ at $sloc }
+sym_alt : sym_alt_ { $1 $ $sloc }
 sym_alt_ :
   | sym_seq_ { $1 }
   | sym_alt BAR sym_seq { AltG (as_alt_sym $1 @ [Elem $3]) }
@@ -667,49 +668,49 @@ sym_alt_ :
 
 sym : sym_alt { $1 }
 
-prod : prod_ { $1 $ at $sloc }
+prod : prod_ { $1 $ $sloc }
 prod_ :
   | sym ARROW2 exp premise_list { ($1, $3, $4) }
 
 gram :
-  | dots_list(prod) { $1 $ at $sloc }
+  | dots_list(prod) { $1 $ $sloc }
 
 
 (* Definitions *)
 
-arg : arg_ { ref $1 $ at $sloc }
+arg : arg_ { ref $1 $ $sloc }
 arg_ :
   | exp_bin { ExpA $1 }
   | SYNTAX typ { SynA $2 }
   | GRAMMAR sym { GramA $2 }
 
-param : param_ { $1 $ at $sloc }
+param : param_ { $1 $ $sloc }
 param_ :
   | varid_bind COLON typ { ExpP ($1, $3) }
-  | typ { ExpP ("" $ at $sloc, $1) }
+  | typ { ExpP ("" $ $sloc, $1) }
   | SYNTAX varid_bind { SynP $2 }
   | GRAMMAR gramid COLON typ { GramP ($2, $4) }
 
 
-def : def_ { $1 $ at $sloc }
+def : def_ { $1 $ $sloc }
 def_ :
   | SYNTAX varid_bind ruleid_list hint* EQ deftyp
     { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
-      SynD ($2, id $ at $loc($3), [], $6, $4) }
+      SynD ($2, id $ $loc($3), [], $6, $4) }
   | SYNTAX varid_bind_lparen enter_scope comma_list(param) RPAREN ruleid_list hint* EQ deftyp exit_scope
     { let id = if $6 = "" then "" else String.sub $6 1 (String.length $6 - 1) in
-      SynD ($2, id $ at $loc($6), $4, $9, $7) }
+      SynD ($2, id $ $loc($6), $4, $9, $7) }
   | GRAMMAR varid_bind ruleid_list COLON typ hint* EQ gram
     { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
-      GramD ($2, id $ at $loc($3), [], $5, $8, $6) }
+      GramD ($2, id $ $loc($3), [], $5, $8, $6) }
   | GRAMMAR varid_bind_lparen enter_scope comma_list(param) RPAREN ruleid_list COLON typ hint* EQ gram exit_scope
     { let id = if $6 = "" then "" else String.sub $6 1 (String.length $6 - 1) in
-      GramD ($2, id $ at $loc($6), $4, $8, $11, $9) }
+      GramD ($2, id $ $loc($6), $4, $8, $11, $9) }
   | RELATION relid COLON nottyp hint*
     { RelD ($2, $4, $5) }
   | RULE relid ruleid_list COLON exp premise_list
     { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
-      RuleD ($2, id $ at $loc($3), $5, $6) }
+      RuleD ($2, id $ $loc($3), $5, $6) }
   | VAR varid_bind COLON typ hint*
     { VarD ($2, $4, $5) }
   | DEF DOLLAR defid COLON typ hint*
@@ -724,18 +725,18 @@ def_ :
     { SepD }
   | SYNTAX varid_bind ruleid_list hint*
     { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
-      HintD (SynH ($2, id $ at $loc($3), $4) $ at $sloc) }
+      HintD (SynH ($2, id $ $loc($3), $4) $ $sloc) }
   | SYNTAX varid_bind ruleid_list atomid hint*
-    { HintD (AtomH ($4 $ at $loc($4), $5) $ at $sloc) }
+    { HintD (AtomH ($4 $ $loc($4), $5) $ $sloc) }
   | GRAMMAR varid_bind ruleid_list hint*
     { let id = if $3 = "" then "" else String.sub $3 1 (String.length $3 - 1) in
-      HintD (GramH ($2, id $ at $loc($3), $4) $ at $sloc) }
+      HintD (GramH ($2, id $ $loc($3), $4) $ $sloc) }
   | RELATION relid hint*
-    { HintD (RelH ($2, $3) $ at $sloc) }
+    { HintD (RelH ($2, $3) $ $sloc) }
   | VAR varid hint*
-    { HintD (VarH ($2, $3) $ at $sloc) }
+    { HintD (VarH ($2, $3) $ $sloc) }
   | DEF DOLLAR defid hint*
-    { HintD (DecH ($3, $4) $ at $sloc) }
+    { HintD (DecH ($3, $4) $ $sloc) }
 
 ruleid_list :
   | (* empty *) { "" }
@@ -744,8 +745,10 @@ ruleid_list :
 
 
 hint :
-  | HINT_LPAREN hintid exp RPAREN { {hintid = $2 $ at $loc($2); hintexp = $3} }
-  | HINT_LPAREN hintid RPAREN { {hintid = $2 $ at $loc($2); hintexp = SeqE [] $ at $loc($2)} }
+  | HINT_LPAREN hintid exp RPAREN
+    { {hintid = $2 $ $loc($2); hintexp = $3} }
+  | HINT_LPAREN hintid RPAREN
+    { {hintid = $2 $ $loc($2); hintexp = SeqE [] $ $loc($2)} }
 
 
 (* Scripts *)