X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPt.ml;h=731a2ba7436f70b6c21f7b05ab0e0274118f9071;hb=refs%2Fheads%2Fmatita-lablgtk3;hp=0480c3d26a53fac04b659530acc2295a622565d6;hpb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 0480c3d26..731a2ba74 100644
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -94,6 +94,8 @@ type term =
   | 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
@@ -177,7 +179,7 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list
 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