From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 plugins/extraction/miniml.mli | 49 +++++++++++++++++++++----------------------
 1 file changed, 24 insertions(+), 25 deletions(-)

(limited to 'plugins/extraction/miniml.mli')

diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index db336152..e1e49d92 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -1,14 +1,15 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
-open Pp
 open Names
 open Globnames
 
@@ -82,7 +83,7 @@ type ml_ind_packet = {
 
 type equiv =
   | NoEquiv
-  | Equiv of kernel_name
+  | Equiv of KerName.t
   | RenEquiv of string
 
 type ml_ind = {
@@ -137,13 +138,13 @@ and ml_pattern =
 (*s ML declarations. *)
 
 type ml_decl =
-  | Dind  of mutual_inductive * ml_ind
+  | Dind  of MutInd.t * ml_ind
   | 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
+  | Sind  of MutInd.t * ml_ind
   | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
@@ -153,14 +154,14 @@ type ml_specif =
   | Smodtype of ml_module_type
 
 and ml_module_type =
-  | MTident of module_path
+  | MTident of ModPath.t
   | MTfunsig of MBId.t * ml_module_type * ml_module_type
-  | MTsig of module_path * ml_module_sig
+  | MTsig of ModPath.t * ml_module_sig
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
   | ML_With_type of Id.t list * Id.t list * ml_type
-  | ML_With_module of Id.t list * module_path
+  | ML_With_module of Id.t list * ModPath.t
 
 and ml_module_sig = (Label.t * ml_specif) list
 
@@ -170,9 +171,9 @@ type ml_structure_elem =
   | SEmodtype of ml_module_type
 
 and ml_module_expr =
-  | MEident of module_path
+  | MEident of ModPath.t
   | MEfunctor of MBId.t * ml_module_type * ml_module_expr
-  | MEstruct of module_path * ml_module_structure
+  | MEstruct of ModPath.t * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
 and ml_module_structure = (Label.t * ml_structure_elem) list
@@ -184,11 +185,9 @@ and ml_module =
 (* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
    implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
 
-type ml_structure = (module_path * ml_module_structure) list
+type ml_structure = (ModPath.t * ml_module_structure) list
 
-type ml_signature = (module_path * ml_module_sig) list
-
-type ml_flat_structure = ml_structure_elem list
+type ml_signature = (ModPath.t * ml_module_sig) list
 
 type unsafe_needs = {
   mldummy : bool;
@@ -202,22 +201,22 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
-  file_naming : module_path -> string;
+  file_naming : ModPath.t -> string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
-    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
-    std_ppcmds;
-  pp_struct : ml_structure -> std_ppcmds;
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_struct : ml_structure -> Pp.t;
 
   (* Concerning a possible interface file *)
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
   sig_preamble :
-    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
-    std_ppcmds;
-  pp_sig : ml_signature -> std_ppcmds;
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_sig : ml_signature -> Pp.t;
 
   (* for an isolated declaration print *)
-  pp_decl : ml_decl -> std_ppcmds;
+  pp_decl : ml_decl -> Pp.t;
 
 }
-- 
cgit v1.2.3