last comment was incomplete by mistake.

- Rationale
  The `Implied attribute will mark the eliminators generated by Coq
  7.3.1 added to the contrib of lambdadelta version 1.
  [the latest version of matita generates different eliminators to
   Prop (with dependences) so we cannot reuse them]
  However, these eliminators, even if provided, must not be taken into
  account when calculating the intrinsinc complexity of the contribution
  on the matita side (by the "probe" tool), because they are not taken into
  account on the Coq side, being `Generated by Coq.

  Note that the intrinsinc complexity we are interested in is the one
  accounting just for the user-defined objects in both contributions.

- probe: updated to handle the `Implied attribute

- .depend: updated

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 03672a0c46c2d9c446fb4a6b5075b6c226b239d0..ebf6f8ef5139779ecc517e0fb9ee83568c14880e 100644 (file)
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -105,7 +105,7 @@ type ind_pragma = (* pragmatic of the object *)
    * fields names and if they are coercions and then the coercion arity *)
 
 type source = [ `Generated (* generated by matita *)
-              | `Provided  (* provided by the user directly or from another ITP *)
+              | `Provided  (* provided as defined by the user *)
               | `Implied   (* provided as generated by another ITP *)
               ]