From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Sep 2003 15:39:28 +0000 (+0000)
Subject: string ==> id
X-Git-Tag: v0_0_1~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=48d41935cc96e8898cc5e3da98a1706294b7b411

string ==> id
---

diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml
index 6679cfabb..748944cdf 100644
--- a/helm/ocaml/cic_omdoc/content.ml
+++ b/helm/ocaml/cic_omdoc/content.ml
@@ -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,14 @@ 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_kind : bool;
          inductive_type : 'term;
          inductive_constructors : 'term declaration list
@@ -88,7 +88,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 +100,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 +113,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 +129,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 
        }