We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent eb1ac32 commit e93a9daCopy full SHA for e93a9da
1 file changed
src/Comparse.Tactic.GenerateParser.fst
@@ -857,10 +857,11 @@ let gen_parser_aux type_fv force_smt =
857
lb_def = parser_fun;
858
} in
859
let sv = pack_sigelt (Sg_Let { isrec = false; lbs = [parser_letbinding];}) in
860
- let sv =
861
- if is_opaque then set_sigelt_attrs [(`"opaque_to_smt")] sv
862
- else sv
+ let attrs = splice_attrs () in
+ let attrs =
+ if is_opaque then attrs @ [(`"opaque_to_smt"); (`tac_opaque)] else attrs
863
in
864
+ let sv = set_sigelt_attrs attrs sv in
865
[sv]
866
867
val gen_parser: term -> Tac decls
0 commit comments