Modulification of identifier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 13 deletions

diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index d170acbb0..14a30ae79 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -65,11 +65,11 @@ type inductive_kind =
 *)
 
 type ml_ind_packet = {
-  ip_typename : identifier;
-  ip_consnames : identifier array;
+  ip_typename : Id.t;
+  ip_consnames : Id.t array;
   ip_logical : bool;
   ip_sign : signature;
-  ip_vars : identifier list;
+  ip_vars : Id.t list;
   ip_types : (ml_type list) array
 }
 
@@ -91,8 +91,8 @@ type ml_ind = {
 
 type ml_ident =
   | Dummy
-  | Id of identifier
-  | Tmp of identifier
+  | Id of Id.t
+  | Tmp of Id.t
 
 (** We now store some typing information on constructors
     and cases to avoid type-unsafe optimisations. This will be
@@ -116,7 +116,7 @@ and ml_ast =
   | MLcons   of ml_type * global_reference * ml_ast list
   | MLtuple  of ml_ast list
   | MLcase   of ml_type * ml_ast * ml_branch array
-  | MLfix    of int * identifier array * ml_ast array
+  | MLfix    of int * Id.t array * ml_ast array
   | MLexn    of string
   | MLdummy
   | MLaxiom
@@ -133,13 +133,13 @@ and ml_pattern =
 
 type ml_decl =
   | Dind  of mutual_inductive * ml_ind
-  | Dtype of global_reference * identifier list * ml_type
+  | Dtype of global_reference * Id.t list * ml_type
   | Dterm of global_reference * ml_ast * ml_type
   | Dfix  of global_reference array * ml_ast array * ml_type array
 
 type ml_spec =
   | Sind  of mutual_inductive * ml_ind
-  | Stype of global_reference * identifier list * ml_type option
+  | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
 type ml_specif =
@@ -154,8 +154,8 @@ and ml_module_type =
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
-  | ML_With_type of identifier list * identifier list * ml_type
-  | ML_With_module of identifier list * module_path
+  | ML_With_type of Id.t list * Id.t list * ml_type
+  | ML_With_module of Id.t list * module_path
 
 and ml_module_sig = (label * ml_specif) list
 
@@ -191,13 +191,13 @@ type unsafe_needs = {
 }
 
 type language_descr = {
-  keywords : Idset.t;
+  keywords : Id.Set.t;
 
   (* Concerning the source file *)
   file_suffix : string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
-    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
     std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
@@ -205,7 +205,7 @@ type language_descr = {
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
   sig_preamble :
-    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
     std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;