-let out_arg = function
- | C.Aux _ -> "aux"
- | C.Premise _ -> "premise"
- | C.Lemma _ -> "lemma"
- | C.Term _ -> "term"
- | C.ArgProof _ -> "proof"
- | C.ArgMethod _ -> "method"
+let mk_theorem name t =
+ let obj = N.Theorem (`Theorem, name, t, None) in
+ G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+
+let mk_tactic tactic =
+ G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None))