Identifier added to inductiveType in the DTD.

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index f0bccf6eaa62f1d5cea5567214035fd3026458b2..fd46c22b4820e74232d3e18e2e8a2eb46b073041 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -158,7 +158,7 @@ and annobj =
     anninductiveType list *                         (* inductive types ,      *)
     UriManager.uri list * int                       (*  parameters,n ind. pars*)
 and anninductiveType = 
- string * bool * annterm *                    (* typename, inductive, arity *)
+ id * string * bool * annterm *               (* typename, inductive, arity *)
   annconstructor list                         (*  constructors              *)
 and annconstructor =
  string * annterm                             (* id, type *)

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index 426ecf21a4d5671001cdfc4a25f4d7892b2b167e..15bc2b9350f88f090cc2a538c06bf78c8cd0e128 100644 (file)
--- a/helm/ocaml/cic/cicParser2.ml
+++ b/helm/ocaml/cic/cicParser2.ml
@@ -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 *)

diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml
index c27a9d576bc225c4f15b8eca40b6d9d8a1dc142f..df59305fea29d1af45a52dc3f771234775e94448 100644 (file)
--- a/helm/ocaml/cic/deannotate.ml
+++ b/helm/ocaml/cic/deannotate.ml
@@ -82,7 +82,7 @@ and deannotate_coinductiveFun (_,name,ty,bo) =
  (name, deannotate_term ty, deannotate_term bo)
 ;;
 
-let deannotate_inductiveType (name, isinductive, arity, cons) =
+let deannotate_inductiveType (_, name, isinductive, arity, cons) =
  (name, isinductive, deannotate_term arity,
   List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
 ;;
@@ -119,6 +119,6 @@ let deannotate_obj =
        deannotate_term bo,deannotate_term ty,params
       )
    | C.AInductiveDefinition (_, tys, params, parno) ->
-      C.InductiveDefinition ( List.map deannotate_inductiveType tys,
+      C.InductiveDefinition (List.map deannotate_inductiveType tys,
        params, parno)
 ;;

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index bffa4b0fc900c3a2f74bb78ebe842afb91fff766..353ef1f7496082b445329372061f59c56ce83d06 100644 (file)
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -93,7 +93,7 @@ let print_term i2a =
   aux
 ;;
 
-let print_mutual_inductive_type i2a (_,_,arity,constructors) =
+let print_mutual_inductive_type i2a (_,_,_,arity,constructors) =
  [< print_term i2a arity ;
     List.fold_right
      (fun (name,ty) i -> [< print_term i2a ty ; i >]) constructors [<>]

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 14ba1da50ff8645e291f6289c03a03a88eafc23c..b20fbd5c03a946f11f7c6e94e7ef5c10c7d5f6f3 100644 (file)
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -136,7 +136,7 @@ let get_ids_to_targets annobj =
       | C.AInductiveDefinition (id,itl,_,_) ->
          set_target id (C.Object annobj) ;
          List.iter
-          (function (_,_,arity,cl) ->
+          (function (_,_,_,arity,cl) ->
             add_target_term arity ;
             List.iter (function (_,ty) -> add_target_term ty) cl
           ) itl