From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Apr 2008 13:42:39 +0000 (+0000)
Subject: added comment
X-Git-Tag: make_still_working~5335
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a685d0ed0394bedc4cc0949bad643e0b1fce0c4;p=helm.git

added comment
---

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 *)