- New attribute `Implied put beside `Generated and `Provided.

[helm.git] / matita / components / ng_kernel / nCic.ml

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 94dc827c810df412dc5d3c4a5a545885bc5a8058..03672a0c46c2d9c446fb4a6b5075b6c226b239d0 100644 (file)
--- 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 by the user directly or from another ITP *)
+              | `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 =