ocaml 3.09 transition

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

diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml
index a09e25cf2b3b46323192d4744e28fcaa95be7d4a..9687e53fc47133866ed63e006aa041e69611a1e6 100644 (file)
--- 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 ;
@@ -123,16 +124,24 @@ and 'term conclude_item =
 and 'term arg =
          Aux of string
        | Premise of premise
+       | Lemma of lemma
        | Term of 'term
        | ArgProof of 'term proof
        | 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: id;
+         lemma_name: string;
+         lemma_uri: string 
+       }
+
 ;;
  
 type 'term conjecture = id * int * 'term context * 'term
@@ -140,7 +149,6 @@ type 'term conjecture = id * int * 'term context * 'term
 and 'term context = 'term hypothesis list
 
 and 'term hypothesis =
- id *
  ['term decl_context_element | ('term,'term proof) def_context_element ] option
 ;;