summaryrefslogtreecommitdiff
path: root/toplevel/ind_tables.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/ind_tables.ml')
-rw-r--r--toplevel/ind_tables.ml34
1 files changed, 20 insertions, 14 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 53c3bcea..77cfa6fa 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ind_tables.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* File created by Vincent Siles, Oct 2007, extended into a generic
support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
@@ -53,7 +51,7 @@ let discharge_scheme (_,(kind,l)) =
Some (kind,Array.map (fun (ind,const) ->
(Lib.discharge_inductive ind,Lib.discharge_con const)) l)
-let (inScheme,_) =
+let inScheme : string * (inductive * constant) array -> obj =
declare_object {(default_object "SCHEME") with
cache_function = cache_scheme;
load_function = (fun _ -> cache_scheme);
@@ -88,8 +86,9 @@ let scheme_object_table =
(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
let declare_scheme_object s aux f =
- (try check_ident ("ind"^s) with _ ->
- error ("Illegal induction scheme suffix: "^s));
+ (try check_ident ("ind"^s)
+ with e when Errors.noncritical e ->
+ error ("Illegal induction scheme suffix: "^s));
let key = if aux = "" then s else aux in
try
let _ = Hashtbl.find scheme_object_table key in
@@ -111,21 +110,28 @@ let declare_individual_scheme_object s ?(aux="") f =
let declare_scheme kind indcl =
Lib.add_anonymous_leaf (inScheme (kind,indcl))
+let is_visible_name id =
+ try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true
+ with Not_found -> false
+
+let compute_name internal id =
+ match internal with
+ | KernelVerbose | UserVerbose -> id
+ | KernelSilent ->
+ Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+
let define internal id c =
- (* TODO: specify even more by distinguish between KernelVerbose and
- * UserVerbose *)
- let fd = match internal with
- | KernelSilent -> declare_internal_constant
- | _ -> declare_constant in
+ let fd = declare_constant ~internal in
+ let id = compute_name internal id in
let kn = fd id
(DefinitionEntry
{ const_entry_body = c;
+ const_entry_secctx = None;
const_entry_type = None;
- const_entry_opaque = false;
- const_entry_boxed = Flags.boxed_definitions() },
+ const_entry_opaque = false },
Decl_kinds.IsDefinition Scheme) in
(match internal with
- | KernelSilent -> ()
+ | KernelSilent -> ()
| _-> definition_message id);
kn