]> matita.cs.unibo.it Git - helm.git/commitdiff
added comment
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Apr 2008 13:42:39 +0000 (13:42 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Apr 2008 13:42:39 +0000 (13:42 +0000)
helm/software/components/ng_kernel/nCic.ml

index c4163edb41d9df73ede9068d8ea7cffdbb347a5f..f32f6842638e196c3a74db75ea1761d0fbfd58e4 100644 (file)
@@ -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 *)