Fix formatting bug in core-spec.
authorRichard Eisenberg <eir@cis.upenn.edu>
Thu, 18 Sep 2014 21:00:37 +0000 (17:00 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Thu, 18 Sep 2014 21:01:10 +0000 (17:01 -0400)
docs/core-spec/CoreLint.ott
docs/core-spec/CoreSyn.ott
docs/core-spec/core-spec.pdf

index 4c51a05..56b4b99 100644 (file)
@@ -247,7 +247,7 @@ G |-co g t0 : s[m |-> t0] ~R k t[n |-> t0]
 
 C = T_R0 </ axBranchkk // kk />
 0 <= ind < length </ axBranchkk // kk />
-forall </ ni_Ri // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind]
+forall </ ni_^^Ri // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind]
 </ G |-co gi : s'i ~Ri k'i t'i // i />
 </ substi @ // i /> = inits(</ [ ni |-> s'i ] // i />)
 </ ni = zi_ki // i />
@@ -536,4 +536,4 @@ forall </ n'i_R'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind
 unify(</ tj // j />, </ t'j // j />) = subst
 subst(s) = subst(s')
 ----------------------------------------- :: CompatCoincident
-no_conflict(C, </ sj // j />, ind1, ind2)
\ No newline at end of file
+no_conflict(C, </ sj // j />, ind1, ind2)
index 56594ec..0c5b304 100644 (file)
@@ -235,6 +235,8 @@ type_list :: 'TypeList_' ::= {{ com List of types }}
 RA {{ tex {\!\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }}
   | _ R                    :: M :: annotation
   {{ tex {\!\!\!{}_{[[R]]} } }}
+  | _ ^^ R                 :: M :: spaced_annotation
+  {{ tex {}_{[[R]]} }}
 
 role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of roles }}
   | </ Ri // , // i />       ::   :: List
index 5d9f29c..52f2e39 100644 (file)
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ