+ (** schematic representation of items scripts are made of *)
+type script_item =
+ [ `Tactic (** action on proof status *)
+ | `Theorem (** start of proof, to be proved *)
+ | `Qed of UriManager.uri (** end of proof, successfull *)
+ | `Def of UriManager.uri (** constant with body *)
+ | `Inductive of UriManager.uri (** inductive definition *)
+ ]
+