let mk_statement flavour name t v =
let name = match name with Some name -> name | None -> assert false in
- let obj = N.Theorem (flavour, name, t, v) in
+ let obj = N.Theorem (flavour, name, t, v, `Regular) in
G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
let mk_qed =