+ verbatim:
+ | comment { $1 }
+ | inner_skip { $1 }
+ | ABBR { $1 }
+ | IN { $1 }
+ | OP { $1 }
+ | CP { $1 }
+ | SPC { $1 }
+ ;
+ verbatims:
+ | { "" }
+ | verbatim verbatims { $1 ^ $2 }
+ ;
+
+/* PROOF STEPS **************************************************************/
+
+ step:
+ | macro_step { $1 }
+ | skips FS { snd $1 }
+ ;
+ steps:
+ | step spcs { $1 }
+ | step spcs steps { $1 @ $3 }
+ ;
+ just:
+ | steps qed { $1 }
+ | proof fs steps qed { $3 }
+ | proof skips { snd $2 }
+ | proof wh skips fs steps qed { snd $3 @ $5 }
+ ;
+ macro_step:
+ | th ident opt_lskips def xskips FS
+ { out "TH" $2;
+ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+ }
+ | th ident lskips fs just FS
+ { out "TH" $2;
+ $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+ }
+ | gen ident def xskips FS
+ { out "TH" $2;
+ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+ }
+ | mor ident cn ident fs just FS
+ { out "MOR" $4; $6 @ mk_morphism (trim $4) }
+ | xlet ident opt_lskips def xskips FS
+ { out "TH" $2;
+ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+ }
+ | xlet ident lskips fs just FS
+ { out "TH" $2;
+ $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+ }
+ | var idents cn xskips FS
+ { out "VAR" (cat $2); mk_vars true $2 }
+ | ax idents cn xskips FS
+ { out "AX" (cat $2); mk_vars false $2 }
+ | ind ident skips FS
+ { out "IND" $2;
+ T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
+ }
+ | sec ident FS
+ { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
+ | xend ident FS
+ { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
+ | unx xskips FS
+ { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
+ | req xp ident FS
+ { out "REQ" $3; [T.Include (trim $3)] }
+ | req ident FS
+ { out "REQ" $2; [T.Include (trim $2)] }
+ | load str FS
+ { out "REQ" $2; [T.Include (strip2 (trim $2))] }
+ | coerc qid spcs skips FS
+ { out "COERCE" (hd $2); coercion (hd $2) }
+ | id coerc qid spcs skips FS
+ { out "COERCE" (hd $3); coercion (hd $3) }
+ | th ident error
+ { out "ERROR" $2; failwith ("macro_step " ^ $2) }
+ | ind ident error
+ { out "ERROR" $2; failwith ("macro_step " ^ $2) }
+ | var idents error
+ { let vs = cat $2 in
+ out "ERROR" vs; failwith ("macro_step " ^ vs) }
+ | ax idents error
+ { let vs = cat $2 in
+ out "ERROR" vs; failwith ("macro_step " ^ vs) }
+ ;
+
+/* VERNACULAR ITEMS *********************************************************/
+
+ item:
+ | OQ verbatims CQ { [T.Comment $2] }
+ | macro_step { $1 }
+ | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
+ | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) }
+ | error { out "ERROR" "item"; failwith "item" }
+ ;
+ items:
+ | rspcs EOF { [] }
+ | rspcs item items { $2 @ $3 }
+ ;
+
+
+/*