diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 7375f2d4..a8ab4fd3 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -1,15 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Libnames +open Globnames open Miniml -open Mlutil open Pp (** By default, in module Format, you can do horizontal placing of blocks @@ -33,17 +32,17 @@ val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val pr_binding : identifier list -> std_ppcmds +val pr_binding : Id.t list -> std_ppcmds -val rename_id : identifier -> Idset.t -> identifier +val rename_id : Id.t -> Id.Set.t -> Id.t -type env = identifier list * Idset.t +type env = Id.t list * Id.Set.t val empty_env : unit -> env -val rename_vars: Idset.t -> identifier list -> env -val rename_tvars: Idset.t -> identifier list -> identifier list -val push_vars : identifier list -> env -> identifier list * env -val get_db_name : int -> env -> identifier +val rename_vars: Id.Set.t -> Id.t list -> env +val rename_tvars: Id.Set.t -> Id.t list -> Id.t list +val push_vars : Id.t list -> env -> Id.t list * env +val get_db_name : int -> env -> Id.t type phase = Pre | Impl | Intf @@ -63,13 +62,13 @@ val top_visible_mp : unit -> module_path val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit -val check_duplicate : module_path -> label -> string +val check_duplicate : module_path -> Label.t -> string type reset_kind = AllButExternal | Everything val reset_renaming_tables : reset_kind -> unit -val set_keywords : Idset.t -> unit +val set_keywords : Id.Set.t -> unit (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) @@ -80,4 +79,5 @@ val mk_ind : string -> string -> mutual_inductive the constants are directly turned into chars *) val is_native_char : ml_ast -> bool +val get_native_char : ml_ast -> char val pp_native_char : ml_ast -> std_ppcmds |