ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_omdoc / content.mli

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index fea233da0d2d321511db9a8d74d46a018e339faa..c1122b8f2b2627d67dccd9ccd3fd4a4e0643af16 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -36,7 +36,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 
@@ -45,14 +45,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
@@ -79,7 +80,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
        }
@@ -91,7 +92,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
@@ -99,12 +100,12 @@ type 'term proof =
 
 and 'term in_proof_context_element =
        [ 'term decl_context_element
-       | ('term,'term proof) def_context_element
+       | ('term,'term proof) def_context_element 
        | ('term,'term proof) joint_context_element
        ]
 
 and 'term conclude_item =
-       { conclude_id :string; 
+       { conclude_id : id; 
          conclude_aref : string;
          conclude_method : string;
          conclude_args : ('term arg) list ;
@@ -120,16 +121,16 @@ 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 
+         lemma_uri: string
        }
 ;;