| Uri of string * subst list option (* as Ident, for long names *)
| NRef of NReference.reference
+ | NCic of NCic.term
+
(* Syntax pattern extensions *)
| Literal of literal
type 'term obj =
| Inductive of 'term capture_variable list * 'term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of Cic.object_flavour * string * 'term * 'term option
+ | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage