X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=f32f6842638e196c3a74db75ea1761d0fbfd58e4;hb=7fa28badba2091f1e3d207f13743a1f68d6bf1f3;hp=c4163edb41d9df73ede9068d8ea7cffdbb347a5f;hpb=013dba0f27e3e834bb2297bcd89a570df6372ef2;p=helm.git diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index c4163edb4..f32f68426 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -60,6 +60,7 @@ type substitution = (int * subst_entry) list type relevance = bool list (* relevance of arguments for conversion *) + (* relevance, name, recno, ty, bo *) type inductiveFun = relevance * string * int * term * term (* if coinductive, the int has no meaning and must be set to -1 *)