X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCic.ml;h=fa204588dc2dd3e5e08ac4558f1d0a1c5e7b73bf;hb=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;hp=4490ee0485c218a4b7681d5c3c0048c45198abd9;hpb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;p=helm.git

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 4490ee048..fa204588d 100644
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -87,7 +87,7 @@ type inductiveType =
  (* relevance, typename, arity, constructors *)
 
 type def_flavour = (* presentational *)
-  [ `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ]
+  [ `Axiom | `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ]
 
 type def_pragma = (* pragmatic of the object *)
   [ `Coercion of int