cic module removed (RIP)

[helm.git] / matita / components / content / notationPt.ml

diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index 90990300abfc6b985bb5266b2ff5800987e53110..aa83b20f33cae6066b4a8392e3151901a1a9595b 100644 (file)
--- a/matita/components/content/notationPt.ml
+++ b/matita/components/content/notationPt.ml
@@ -178,7 +178,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 * NCic.def_pragma
+  | Theorem of NCic.def_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