]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicParser2.ml
lazily ==> call_by_name (since it is really a call_by_name!)
[helm.git] / helm / ocaml / cic / cicParser2.ml
index 426ecf21a4d5671001cdfc4a25f4d7892b2b167e..15bc2b9350f88f090cc2a538c06bf78c8cd0e128 100644 (file)
@@ -163,10 +163,11 @@ let rec get_inductive_types =
   | he::tl ->
      let tyname    = string_of_attr (he#attribute "name")
      and inductive = bool_of_attr   (he#attribute "inductive")
+     and xid = string_of_attr (he#attribute "id")
      and (arity,cons) =
       get_names_arity_constructors (he#sub_nodes)
      in
-      (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
+      (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
 ;;
 
 (* This is the main function and also the only one used directly from *)