X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPt.ml;h=087a43ddea8e4325b9769acc850eae77491a087f;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=cead5e7ae8eda28cc6ec9d5fc8262b522ae6f3b6;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index cead5e7ae..087a43dde 100644
--- a/matita/components/content/notationPt.ml
+++ b/matita/components/content/notationPt.ml
@@ -177,8 +177,8 @@ 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 NCic.def_flavour * string * 'term * 'term option * NCic.def_pragma
-      (** flavour, name, type, body
+  | Theorem of string * 'term * 'term option * NCic.c_attr
+      (** name, type, body, attributes
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage
        * - body is present when its given along with the command, otherwise it