X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCic.ml;h=ebf6f8ef5139779ecc517e0fb9ee83568c14880e;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=7e4e4f85535dfd76beb667fa2bc475325a699438;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 7e4e4f855..ebf6f8ef5 100644
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -94,6 +94,7 @@ type def_pragma = (* pragmatic of the object *)
   | `Elim of sort       (* elimination principle; universe is not relevant *)
   | `Projection         (* record projection *)
   | `InversionPrinciple (* inversion principle *)
+  | `DiscriminationPrinciple (* discrimination principle *)
   | `Variant 
   | `Local 
   | `Regular ]            (* Local = hidden technicality *)
@@ -103,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 source = [ `Generated (* generated by matita *)
+              | `Provided  (* provided as defined by the user *)
+              | `Implied   (* provided as generated by another ITP *)
+              ]
 
-type c_attr = generated * def_flavour * def_pragma
-type f_attr = generated * def_flavour * def_pragma
-type i_attr = generated * ind_pragma
+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 =