let strip1 s =
String.sub s 1 (String.length s - 1)
+
+ let coercion str =
+ [T.Coercion (false, str); T.Coercion (true, str)]
+
+ let notation str =
+ [T.Notation (false, str); T.Notation (true, str)]
%}
%token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
%token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
;
field:
| ident cn unexports_r
- { $1 ^ $2 ^ fst $3, snd $3 }
+ { $1 ^ $2 ^ fst $3, snd $3 }
| ident coe unexports_r
- { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion (trim $1)] }
+ { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
;
fields:
| field { $1 }
| load str FS
{ out "REQ" $2; [T.Include (strip2 (trim $2))] }
| coerc qid spcs cn unexports FS
- { out "COERCE" (hd $2); [T.Coercion (hd $2)] }
+ { out "COERCE" (hd $2); coercion (hd $2) }
| id coerc qid spcs cn unexports FS
- { out "COERCE" (hd $3); [T.Coercion (hd $3)] }
+ { out "COERCE" (hd $3); coercion (hd $3) }
| th ident error
{ out "ERROR" $2; failwith ("macro_step " ^ $2) }
| ind ident error
| OQ verbatims CQ { [T.Comment $2] }
| macro_step { $1 }
| set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
- | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ trim $3)] }
+ | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
| error { out "ERROR" "item"; failwith "item" }
;
items: