From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 5 Sep 2015 15:36:06 +0000 (+0000)
Subject: last comment was incomplete by mistake.
X-Git-Tag: make_still_working~699
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git

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 03672a0c4..ebf6f8ef5 100644
--- 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 *)
               ]