From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/table.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 16c2275f1..fbf48889f 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -15,7 +15,7 @@ open Declarations module Refset' : Set.S with type elt = global_reference module Refmap' : Map.S with type key = global_reference -val safe_basename_of_global : global_reference -> identifier +val safe_basename_of_global : global_reference -> Id.t (*s Warning and Error messages. *) @@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a -val error_singleton_become_prop : identifier -> 'a +val error_singleton_become_prop : Id.t -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a @@ -193,12 +193,12 @@ val extract_inductive : reference -> string -> string list -> string option -> unit -type int_or_id = ArgInt of int | ArgId of identifier +type int_or_id = ArgInt of int | ArgId of Id.t val extraction_implicit : reference -> int_or_id list -> unit (*s Table of blacklisted filenames *) -val extraction_blacklist : identifier list -> unit +val extraction_blacklist : Id.t list -> unit val reset_extraction_blacklist : unit -> unit val print_extraction_blacklist : unit -> Pp.std_ppcmds -- cgit v1.2.3