X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent.ml;h=9687e53fc47133866ed63e006aa041e69611a1e6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6679cfabb466e35758710a6edeba0f542e9448fa;hpb=7fd0b9edc6be316b4ef43ca98a6b02f76dd1108e;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml
index 6679cfabb..9687e53fc 100644
--- a/helm/ocaml/cic_omdoc/content.ml
+++ b/helm/ocaml/cic_omdoc/content.ml
@@ -28,7 +28,7 @@
 (*                           PROJECT HELM                                 *)
 (*                                                                        *)
 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             16/62003                                   *)
+(*                             16/6/2003                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -45,7 +45,7 @@ type var_or_const = Var | Const;;
 
 type 'term declaration =
        { dec_name : string option;
-         dec_id : string ;
+         dec_id : id ;
          dec_inductive : bool;
          dec_aref : string;
          dec_type : 'term 
@@ -54,14 +54,15 @@ type 'term declaration =
 
 type 'term definition =
        { def_name : string option;
-         def_id : string ;
+         def_id : id ;
          def_aref : string ;
          def_term : 'term 
        }
 ;;
 
 type 'term inductive =
-       { inductive_id : string ;
+       { inductive_id : id ;
+         inductive_name : string;
          inductive_kind : bool;
          inductive_type : 'term;
          inductive_constructors : 'term declaration list
@@ -88,7 +89,7 @@ type ('term,'proof) in_joint_context_element =
 ;;
 
 type ('term,'proof) joint =
-       { joint_id : string ;
+       { joint_id : id ;
          joint_kind : joint_recursion_kind ;
          joint_defs : ('term,'proof) in_joint_context_element list
        }
@@ -100,7 +101,7 @@ type ('term,'proof) joint_context_element =
 
 type 'term proof = 
       { proof_name : string option;
-        proof_id   : string ;
+        proof_id   : id ;
         proof_context : 'term in_proof_context_element list ;
         proof_apply_context: 'term proof list;
         proof_conclude : 'term conclude_item
@@ -113,7 +114,7 @@ and 'term in_proof_context_element =
        ]
 
 and 'term conclude_item =
-       { conclude_id :string; 
+       { conclude_id : id; 
          conclude_aref : string;
          conclude_method : string;
          conclude_args : ('term arg) list ;
@@ -129,14 +130,14 @@ and 'term arg =
        | ArgMethod of string (* ???? *)
 
 and premise =
-       { premise_id: string;
+       { premise_id: id;
          premise_xref : string ;
          premise_binder : string option;
          premise_n : int option;
        }
 
 and lemma =
-       { lemma_id: string;
+       { lemma_id: id;
          lemma_name: string;
          lemma_uri: string 
        }