From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Nov 2002 09:52:01 +0000 (+0000)
Subject: Identifier added to inductiveType in the DTD.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76a7d625c7eacd8f872485f24066a79a87156c92;p=helm.git

Identifier added to inductiveType in the DTD.
---

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index f0bccf6ea..fd46c22b4 100644
--- 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 426ecf21a..15bc2b935 100644
--- 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 c27a9d576..df59305fe 100644
--- 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 bffa4b0fc..353ef1f74 100644
--- 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 14ba1da50..b20fbd5c0 100644
--- 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