From d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 5 Sep 2015 15:36:06 +0000 Subject: [PATCH] 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 --- matita/components/ng_kernel/nCic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 *) ] -- 2.39.2