X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCic.ml;h=ebf6f8ef5139779ecc517e0fb9ee83568c14880e;hb=cdb85e803cd6038352ec0a318285f96f42faf02d;hp=94dc827c810df412dc5d3c4a5a545885bc5a8058;hpb=5a88ca4db8f9d97a58add90a8a23f06960d9364f;p=helm.git

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 94dc827c8..ebf6f8ef5 100644
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -104,11 +104,14 @@ type ind_pragma = (* pragmatic of the object *)
   (* inductive type that encodes a record; the arguments are the record 
    * fields names and if they are coercions and then the coercion arity *)
 
-type generated = [ `Generated | `Provided ]
-
-type c_attr = generated * def_flavour * def_pragma
-type f_attr = generated * def_flavour * def_pragma
-type i_attr = generated * ind_pragma
+type source = [ `Generated (* generated by matita *)
+              | `Provided  (* provided as defined by the user *)
+              | `Implied   (* provided as generated by another ITP *)
+              ]
+
+type c_attr = source * def_flavour * def_pragma
+type f_attr = source * def_flavour * def_pragma
+type i_attr = source * ind_pragma
 
  (* invariant: metasenv and substitution have disjoint domains *)
 type obj_kind =